Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.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 | d09437fcfc7c |
comparison
equal
deleted
inserted
replaced
234:e06b76e5b682 | 235:846e0926bb89 |
---|---|
488 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X | 488 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X |
489 choice-func' X p∨¬p not = have_to_find where | 489 choice-func' X p∨¬p not = have_to_find where |
490 ψ : ( ox : Ordinal ) → Set (suc n) | 490 ψ : ( ox : Ordinal ) → Set (suc n) |
491 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X | 491 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X |
492 lemma-ord : ( ox : Ordinal ) → ψ ox | 492 lemma-ord : ( ox : Ordinal ) → ψ ox |
493 lemma-ord ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where | 493 lemma-ord ox = TransFinite {ψ} induction ox where |
494 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 494 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
495 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) | 495 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) |
496 ∋-p A x | case1 (lift t) = yes t | 496 ∋-p A x | case1 (lift t) = yes t |
497 ∋-p A x | case2 t = no (λ x → t (lift x )) | 497 ∋-p A x | case2 t = no (λ x → t (lift x )) |
498 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } | 498 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } |
528 Union = ZF.Union OD→ZF | 528 Union = ZF.Union OD→ZF |
529 Power = ZF.Power OD→ZF | 529 Power = ZF.Power OD→ZF |
530 Select = ZF.Select OD→ZF | 530 Select = ZF.Select OD→ZF |
531 Replace = ZF.Replace OD→ZF | 531 Replace = ZF.Replace OD→ZF |
532 isZF = ZF.isZF OD→ZF | 532 isZF = ZF.isZF OD→ZF |
533 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) |