Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 235:846e0926bb89
fix cardinal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 15 Aug 2019 04:51:24 +0900 |
| parents | e06b76e5b682 |
| children | 650bdad56729 |
comparison
equal
deleted
inserted
replaced
| 234:e06b76e5b682 | 235:846e0926bb89 |
|---|---|
| 53 | 53 |
| 54 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) | 54 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) |
| 55 | 55 |
| 56 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) | 56 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) |
| 57 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where | 57 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where |
| 58 lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt | |
| 59 lemma : Ordinal → Ordinal | 58 lemma : Ordinal → Ordinal |
| 60 lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y) | 59 lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) |
| 61 lemma y | p | no n = o∅ | 60 lemma y | p | no n = o∅ |
| 62 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) | 61 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) |
| 63 ... | t with decp ( x ≡ π1 t ) | 62 ... | t with decp ( x ≡ π1 t ) |
| 64 ... | yes _ = π2 t | 63 ... | yes _ = π2 t |
| 65 ... | no _ = o∅ | 64 ... | no _ = o∅ |
| 69 | 68 |
| 70 | 69 |
| 71 -- contra position of sup-o< | 70 -- contra position of sup-o< |
| 72 -- | 71 -- |
| 73 | 72 |
| 74 postulate | 73 -- postulate |
| 75 -- contra-position of mimimulity of supermum required in Cardinal | 74 -- -- contra-position of mimimulity of supermum required in Cardinal |
| 76 sup-x : ( Ordinal → Ordinal ) → Ordinal | 75 -- sup-x : ( Ordinal → Ordinal ) → Ordinal |
| 77 sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) | 76 -- sup-lb : { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) |
| 78 | 77 |
| 79 ------------ | 78 ------------ |
| 80 -- | 79 -- |
| 81 -- Onto map | 80 -- Onto map |
| 82 -- def X x -> xmap | 81 -- def X x -> xmap |