Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 577:cfb26091e806

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... look bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jun 2022 23:57:46 +0900
parents 59c11152f604
children cc399a8602db
files src/zorn.agda
diffstat 1 files changed, 1 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Sun Jun 05 22:49:04 2022 +0900
+++ b/src/zorn.agda	Sun Jun 05 23:57:46 2022 +0900
@@ -248,6 +248,7 @@
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
       fc∨sup :  {a : Ordinal } → a o< osuc z →  ( ca : odef chain a ) → IsSup A chain  ( chain⊆A ca) ∨ HasPrev A chain ( chain⊆A ca) f  
+      mono : { a : Ordinal } → (ca : odef chain a) → (SA : HOD)  → IsSup A SA (chain⊆A ca) → SA  ⊆' chain 
 
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field