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

comparison OD.agda @ 262:53744836020b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CH trying ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2019 20:26:32 +0900
parents d9d178d1457c
children 2169d948159b
comparison
equal deleted inserted replaced
261:d9d178d1457c 262:53744836020b
359 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 359 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
360 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 360 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
361 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 361 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
362 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy 362 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
363 363
364 -- minimal-2 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
365 -- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
366
364 OD→ZF : ZF 367 OD→ZF : ZF
365 OD→ZF = record { 368 OD→ZF = record {
366 ZFSet = OD 369 ZFSet = OD
367 ; _∋_ = _∋_ 370 ; _∋_ = _∋_
368 ; _≈_ = _==_ 371 ; _≈_ = _==_
545 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} ) 548 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} )
546 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 549 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
547 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 550 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
548 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 551 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
549 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 552 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
553
554 ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x}
555 ord⊆power a x lt = power← (Ord a) x lemma where
556 lemma : {y : OD} → x ∋ y → Ord a ∋ y
557 lemma y<x with osuc-≡< lt
558 lemma y<x | case1 refl = c<→o< y<x
559 lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
560
561 -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x}
562 -- continuum-hyphotheis a x = ?
550 563
551 -- assuming axiom of choice 564 -- assuming axiom of choice
552 regularity : (x : OD) (not : ¬ (x == od∅)) → 565 regularity : (x : OD) (not : ¬ (x == od∅)) →
553 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 566 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
554 proj1 (regularity x not ) = x∋minimal x not 567 proj1 (regularity x not ) = x∋minimal x not