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

changeset 1182:0727cf865ebd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 24 Feb 2023 15:00:23 +0800
parents cf25490dd112
children f5deac708524
files src/BAlgebra.agda src/Topology.agda
diffstat 2 files changed, 7 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Fri Feb 24 11:52:44 2023 +0800
+++ b/src/BAlgebra.agda	Fri Feb 24 15:00:23 2023 +0800
@@ -58,6 +58,11 @@
     lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x
     lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt)  ⟫
 
+∨L＼X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x
+∨L＼X {L} {X} {x} Lx with ODC.∋-p O X (* x)
+... | yes y = case1 ( subst (λ k → odef X k ) &iso y  )
+... | no  n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫
+
 
 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
--- a/src/Topology.agda	Fri Feb 24 11:52:44 2023 +0800
+++ b/src/Topology.agda	Fri Feb 24 15:00:23 2023 +0800
@@ -472,8 +472,8 @@
        cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x)
        ... | case1 p = p
        ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where
-          fp04 : {y : Ordinal} → odef (* X) y → Ordinal
-          fp04 {y} xy = & (L ＼ * y)
+          fp04 : {y x : Ordinal} → odef (* X) y → ¬ odef (L ＼ * y) x
+          fp04 {y} {x} xy ⟪ Lx , nx ⟫ = ?
           fp03 : ?
           fp03 = ?
        no-cover : ¬ ( (* (OX CX)) covers L )