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

comparison src/Topology.agda @ 1104:81b859b678a8

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 Thu, 29 Dec 2022 14:42:28 +0900
parents a9a7ad7784cc
children fabcb7d9f50c
comparison
equal deleted inserted replaced
1103:8df83228d148 1104:81b859b678a8
63 data genTop (P : HOD) : HOD → Set (suc n) where 63 data genTop (P : HOD) : HOD → Set (suc n) where
64 gi : {x : HOD} → P ∋ x → genTop P x 64 gi : {x : HOD} → P ∋ x → genTop P x
65 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y) 65 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
66 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q) 66 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
67 67
68 -- Limit point
69
70 record LP { L : HOD} (top : Topology L) ( S x : HOD ) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
71 field
72 neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD
73 isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )
74
75 -- Finite Intersection Property 68 -- Finite Intersection Property
76 69
77 data Finite-∩ (S : HOD) : HOD → Set (suc n) where 70 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
78 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x 71 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
79 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y) 72 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
164 157
165 -- Product of UFL has limit point (Tychonoff) 158 -- Product of UFL has limit point (Tychonoff)
166 159
167 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) 160 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ)
168 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where 161 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
169 uflp : {L : HOD} (LP : L ⊆ Power (ZFP P Q)) (F : Filter LP) 162 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
170 (uf : ultra-filter {L} {_} {LP} F) → UFLP (TP Top⊗ TQ) LP F uf 163 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
171 uflp {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } 164 uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where
165 lprod : {x y : Ordinal } → (ly : odef L y) → odef (ZFP P Q) x
166 lprod {x} {y} ly = LPQ ly x ?
167 -- LP : HOD
168 -- LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
169 LP : HOD
170 LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) }
171 ; odmax = & P ; <odmax = ? } where
172 L→P : {y : Ordinal } → odef L y → HOD
173 L→P {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ1 (LPQ ly z yz ) ≡ x }
174 ; odmax = & P ; <odmax = ? }
175 LPP : LP ⊆ Power P
176 LPP = ?
177 FP : Filter LPP
178 FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
179 uFP : ultra-filter FP
180 uFP = record { proper = ? ; ultra = ? }
181 LQ : HOD
182 LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) }
183 ; odmax = & P ; <odmax = ? } where
184 L→Q : {y : Ordinal } → odef L y → HOD
185 L→Q {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ2 (LPQ ly z yz ) ≡ x }
186 ; odmax = & Q ; <odmax = ? }
187 LQQ : LQ ⊆ Power Q
188 LQQ = ?
189 uflpp : UFLP {P} TP {LP} LPP FP uFP
190 uflpp = ?
172 191
173 192
174 193
175 194
176 195