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

comparison ordinal-definable.agda @ 138:567084f2278f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 17:37:26 +0900
parents 35ce91192cf4
children 312e27aa3cb5
comparison
equal deleted inserted replaced
137:c7c9f3efc428 138:567084f2278f
417 lemma cond = (proj1 cond) y (proj2 cond) 417 lemma cond = (proj1 cond) y (proj2 cond)
418 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 418 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
419 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where 419 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
420 lemma : def (in-codomain X ψ) (od→ord (ψ x)) 420 lemma : def (in-codomain X ψ) (od→ord (ψ x))
421 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ) ) 421 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ) )
422 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (ψ x == y)) 422 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
423 replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) ) 423 replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) )
424 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 424 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
425 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 425 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
426 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 426 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
427 minimul x not = od∅ 427 minimul x not = od∅
428 regularity : (x : OD) (not : ¬ (x == od∅)) → 428 regularity : (x : OD) (not : ¬ (x == od∅)) →