Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1486:49c3ef1e9b4f
Topology fixed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2024 16:07:57 +0900 |
| parents | 5dacb669f13b |
| children | 1925debf28bb |
| files | src/Topology.agda |
| diffstat | 1 files changed, 25 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Mon Jul 01 15:43:35 2024 +0900 +++ b/src/Topology.agda Mon Jul 01 16:07:57 2024 +0900 @@ -598,17 +598,16 @@ fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx)) fp38 = SB.t⊆i (fp02 tx ux) fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux))) - fp39 {w} txw with ∨L＼X {L} {(SB.i (fp02 tx ux))} (fp40 ux ?) - ... | t = ? - -- ... | case1 sb = sb - -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) + fp39 {w} txw with ∨L＼X {* (SB.i (fp02 tx ux))} (fp40 ux txw) + ... | case1 sb = sb + ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where fp38 : (L ＼ (* (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* ty)) fp38 = SB.t⊆i (fp02 ty uy) fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy))) - fp39 {w} tyw = ? -- with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw) - -- ... | case1 sb = sb - -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) + fp39 {w} tyw with ∨L＼X {* (SB.i (fp02 ty uy))} (fp40 uy tyw) + ... | case1 sb = sb + ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) fp04 {tx} {ty} = ==→o≡ record { eq→ = fp05 ; eq← = fp09 } where fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x @@ -633,7 +632,7 @@ sb : SB (Compact.finCover compact (OOX CX) cov) sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) - no-finite-cover fcovers = ? where -- ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where + no-finite-cover fcovers = ⊥-elim ( o<¬≡ (sym (==→o≡ f22)) f25 ) where f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) f23 = SB.t⊆i sb f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ @@ -655,23 +654,23 @@ fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ ) fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x - fp19 {y} Xy = ? -- with ∨L＼X {L} {* y} {x} Lx - -- ... | case1 yx = yx - -- ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where - -- fp20 : odef (* X) y ∧ odef (L ＼ * y) x - -- fp20 = ⟪ Xy , lyx ⟫ + fp19 {y} Xy with ∨L＼X {* y} {x} Lx + ... | case1 yx = yx + ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where + fp20 : odef (* X) y ∧ odef (L ＼ * y) x + fp20 = ⟪ Xy , lyx ⟫ coverf : {x : Ordinal} → (Lx : odef L x ) → HOD coverf Lx = minimal (coverSet Lx) (fp17 Lx) fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt)) - fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) ? record { z = _ ; az = fp25 ; x=ψz = fp24 } where + fp22 {x} Lx = eq← *iso record { z = _ ; az = fp25 ; x=ψz = fp24 } where fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx))) - fp24 = cong (λ k → & ( L ＼ k )) ? + fp24 = ==→o≡ (＼-cong L L (coverf Lx) (* (& (coverf Lx))) ==-refl (==-sym *iso) ) fp25 : odef (* X) (& (coverf Lx)) fp25 = proj1 ( x∋minimal (coverSet Lx) (fp17 Lx) ) fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x - fp23 {x} Lx = subst (λ k → odef k x) ? ⟪ Lx , fp26 ⟫ where + fp23 {x} Lx = eq← *iso ⟪ Lx , fp26 ⟫ where fp26 : ¬ odef (coverf Lx) x - fp26 = subst (λ k → ¬ odef k x ) ? (proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) )) ) + fp26 llx = proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) )) (eq← *iso llx) limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal limit {X} CX fip with trio< X o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) @@ -712,7 +711,7 @@ f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where f11 : * (Neighbor.u Np) ⊆ * (& q) - f11 {x} ux = subst (λ k → odef k x ) ? ( p⊆q (subst (λ k → odef k x) ? (Neighbor.u⊆v Np ux)) ) + f11 {x} ux = eq← *iso ( p⊆q (eq→ *iso (Neighbor.u⊆v Np ux)) ) f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q) f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where upq : Ordinal @@ -720,20 +719,19 @@ ou : odef (OS TP) upq ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq)) ux : odef (* upq) x - ux = subst ( λ k → odef k x ) ? ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ + ux = eq← *iso ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ f20 : * upq ⊆ * (& (p ∩ q)) - f20 = subst₂ (λ j k → j ⊆ k ) ? ? ( λ {x} pq - → ⟪ subst (λ k → odef k x) ? (Neighbor.u⊆v Np (proj1 pq)) , subst (λ k → odef k x) ? (Neighbor.u⊆v Nq (proj2 pq)) ⟫ ) + f20 {x} lt = eq← *iso ⟪ eq→ *iso (Neighbor.u⊆v Np (proj1 pq)) , eq→ *iso (Neighbor.u⊆v Nq (proj2 pq)) ⟫ where + pq : odef (* (Neighbor.u Np) ∩ * (Neighbor.u Nq)) x + pq = eq→ *iso lt CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q) -CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) ? pqx -... | t = ? --- ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) ? px ) +CAP P {p} {q} Pp Pq x pqx with eq→ *iso pqx +... | ⟪ px , qx ⟫ = Pp _ (eq← *iso px ) NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p ) -NEG P {p} Pp x vx with subst (λ k → odef k x) ? vx -... | t = ? --- ... | ⟪ Px , npx ⟫ = Px +NEG P {p} Pp x vx with eq→ *iso vx +... | ⟪ Px , npx ⟫ = Px