Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1228:e3f20bc4fac9
last part of Tychonoff
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Mar 2023 10:28:55 +0900 |
| parents | 72b5815be243 |
| children | 5e6dfe739f6a |
| files | src/Topology.agda src/Tychonoff.agda |
| diffstat | 2 files changed, 41 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Tue Mar 07 19:19:03 2023 +0900 +++ b/src/Topology.agda Wed Mar 08 10:28:55 2023 +0900 @@ -224,12 +224,14 @@ -- Product Topology is not -- ZFP (OS TP) (OS TQ) (box) +-- Rectangle subset (zπ1 ⁻¹ p) record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where field p : Ordinal op : odef (OS TP) p prod : x ≡ & (ZFP (* p) Q ) +-- Rectangle subset (zπ12⁻¹ q ) record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where field q : Ordinal @@ -287,7 +289,7 @@ data Finite-∪ (S : HOD) : Ordinal → Set n where fin-e : Finite-∪ S o∅ - fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) + fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) -- an element of S fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) -- Finite-∪ S y → Union y ⊆ S @@ -621,8 +623,9 @@ open Filter --- Ultra Filter has limit point - +-- +-- {v | Neighbor lim v} set of u ⊆ v ⊆ P where u is an open set u ∋ x +-- record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where field u : Ordinal
--- a/src/Tychonoff.agda Tue Mar 07 19:19:03 2023 +0900 +++ b/src/Tychonoff.agda Wed Mar 08 10:28:55 2023 +0900 @@ -490,6 +490,8 @@ ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp )) uflp : UFLP TP FP UFP uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP + FPSet⊆F : {x : Ordinal } → odef FPSet x → odef (filter F) (& (ZFP (* x) Q)) + FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ? -- copy and pasted, sorry -- @@ -636,40 +638,47 @@ Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq) + record aSubbase (b : Ordinal) : Set n where + field + fp∋b∨fq∋b : odef (filter FP ) b ∨ odef (filter FP ) b + isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v isL {v} npq = filter1 F (λ z xz → Neighbor.v⊆P npq (subst (λ k → odef k z) *iso xz)) - (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb ?)) ? where + (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb npq pqb⊆opq)) bpq⊆v where + -- + -- Product Topolgy's open set contains a subbase which is an element of ZPF p Q or ZPF P q + -- Neighbor of limit contains an open set which conatins a limit + -- every point of an open set is covered by a subbase + -- so there is a subbase which contains a limit, the subbase is an element of projection of a filter (P or Q) + TPQ = ProductTopology TP TQ + lim = & < * (UFLP.limit uflp) , * (UFLP.limit uflq) > bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) bpq = Neighbor.ou npq (Neighbor.ux npq) pqb : Subbase (pbase TP TQ) (Base.b bpq ) pqb = Base.sb bpq pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq ) + bpq⊆v : * (Base.b bpq) ⊆ * v + bpq⊆v {x} bx = Neighbor.u⊆v npq (pqb⊆opq bx) pqb⊆opq = Base.b⊆u bpq - F∋base : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → odef (filter F) b - F∋base (gi (case1 px)) b⊆u = ? where - -- F is ultra, so F ∋ b ∨ F ∋ (ZFP P Q ＼ b) - -- FP ∋ b ∨ FQ ∋ b - -- Neighbor b ∋ limit - -- F ∋ (ZFP P Q ＼ b) → ¬ Neighbor b ∋ limit → ⊥ - -- F contains no od∅, because it projection contains no od∅ - -- x is an element of BaseP, which is a subset of Neighbor npq - -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp) - -- BaseP ∩ F is not empty - -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , - nei1 : HOD - nei1 = ? -- ZFPproj1 (* (Neighbor.u npq)) (Power P) (Power Q) - plimit : Ordinal - plimit = UFLP.limit uflp - nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b - nproper = {!!} - bp : BaseP {P} TP Q ? - bp = record { p = {!!} ; op = {!!} ; prod = {!!} } - neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F - neip = {!!} - il3 : filter F ∋ {!!} - il3 = {!!} - F∋base (gi (case2 qx)) b⊆u = ? - F∋base (g∩ b1 b2) b⊆u = ? + F∋base : {b v : Ordinal } → Subbase (pbase TP TQ) b → (npq : Neighbor TPQ lim v) → * b ⊆ * (Neighbor.u npq) → odef (filter F) b + F∋base {b} {v} (gi (case1 px)) npq b⊆u = subst (λ k → odef (filter F) k) (sym (BaseP.prod px)) f∋b where + px∋limit : odef (* (BaseP.p px)) (UFLP.limit uflp) + px∋limit = ? + fp∋b : filter FP ∋ * (BaseP.p px) + fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit + ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x } + f∋b : odef (filter F) (& (ZFP (* (BaseP.p px)) Q)) + f∋b = FPSet⊆F (subst (λ k → odef (filter FP) k ) &iso fp∋b ) + F∋base (gi (case2 qx)) npq b⊆u = ? + F∋base (g∩ {x} {y} b1 b2) npq xy⊆u = F∋x∩y where + fb01 : odef (filter F) x + fb01 = F∋base b1 ? ? + fb02 : odef (filter F) y + fb02 = F∋base b2 ? ? + F∋x∩y : odef (filter F) (& (* x ∩ * y)) + F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02) + (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01)) + (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb02)))