Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 262:53744836020b
CH trying ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 22 Sep 2019 20:26:32 +0900 |
parents | d9d178d1457c |
children | 2169d948159b |
line wrap: on
line diff
--- a/OD.agda Tue Sep 17 09:29:27 2019 +0900 +++ b/OD.agda Sun Sep 22 20:26:32 2019 +0900 @@ -361,6 +361,9 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy +-- minimal-2 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) +-- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} ) + OD→ZF : ZF OD→ZF = record { ZFSet = OD @@ -548,6 +551,16 @@ lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) + ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x} + ord⊆power a x lt = power← (Ord a) x lemma where + lemma : {y : OD} → x ∋ y → Ord a ∋ y + lemma y<x with osuc-≡< lt + lemma y<x | case1 refl = c<→o< y<x + lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a + + -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} + -- continuum-hyphotheis a x = ? + -- assuming axiom of choice regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)