Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 227:a4cdfc84f65f
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 11 Aug 2019 18:37:33 +0900 |
parents | 176ff97547b4 |
children | 49736efc822b |
comparison
equal
deleted
inserted
replaced
226:176ff97547b4 | 227:a4cdfc84f65f |
---|---|
46 lemma : Ordinal → Ordinal | 46 lemma : Ordinal → Ordinal |
47 lemma y with p∨¬p ( _⊗_.π1 lt ≡ x ) | 47 lemma y with p∨¬p ( _⊗_.π1 lt ≡ x ) |
48 lemma y | case1 refl = _⊗_.π2 lt | 48 lemma y | case1 refl = _⊗_.π2 lt |
49 lemma y | case2 not = o∅ | 49 lemma y | case2 not = o∅ |
50 | 50 |
51 -- contra position of sup-o< | |
52 -- | |
53 | |
54 record Sup ( ψ : Ordinal → Ordinal ) : Set n where | |
55 field | |
56 sup-x : Ordinal | |
57 sup-lb : {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ sup-x ) | |
58 | |
59 sup-o> : ( ψ : Ordinal → Ordinal ) → Sup ψ | |
60 sup-o> ψ = record { | |
61 sup-x = od→ord ( minimul (Ord (osuc (sup-o ψ))) lemma ) | |
62 ; sup-lb = λ {z} z<sψ → lemma1 z<sψ | |
63 } where | |
64 lemma0 : {x : Ordinal} → o∅ o< osuc x | |
65 lemma0 {x} with trio< o∅ (osuc x) | |
66 lemma0 {x} | tri< a ¬b ¬c = a | |
67 lemma0 {x} | tri≈ ¬a refl ¬c = ⊥-elim (¬x<0 <-osuc ) | |
68 lemma0 {x} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
69 lemma : ¬ (Ord (osuc (sup-o ψ)) == od∅) | |
70 lemma record { eq→ = eq→ ; eq← = eq← } = ¬x<0 {o∅} ( eq→ lemma0 ) | |
71 lemma1 : {z : Ordinal} → z o< sup-o ψ → z o< osuc (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))) | |
72 lemma1 {z} lt with trio< z (ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma))) | |
73 lemma1 {z} lt | tri< a ¬b ¬c = ordtrans a <-osuc | |
74 lemma1 {z} lt | tri≈ ¬a refl ¬c = <-osuc | |
75 lemma1 {z} lt | tri> ¬a ¬b c = ⊥-elim (o<> c lemma2 ) where | |
76 lemma2 : z o< ψ (od→ord (minimul (Ord (osuc (sup-o ψ))) lemma)) | |
77 lemma2 = ordtrans sup-o< ( o<-subst (x∋minimul (Ord (osuc (sup-o ψ))) lemma ) ? ?) | |
78 | |
51 ------------ | 79 ------------ |
52 -- | 80 -- |
53 -- Onto map | 81 -- Onto map |
54 -- def X x -> xmap | 82 -- def X x -> xmap |
55 -- X ---------------------------> Y | 83 -- X ---------------------------> Y |