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

comparison src/Topology.agda @ 1105:fabcb7d9f50c

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 Fri, 30 Dec 2022 20:59:14 +0900
parents 81b859b678a8
children 3b894bbefe92
comparison
equal deleted inserted replaced
1104:81b859b678a8 1105:fabcb7d9f50c
160 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)
161 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
162 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) 162 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
163 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf 163 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
164 uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where 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 165 LP : HOD
170 LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) } 166 LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
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 167 LPP : LP ⊆ Power P
176 LPP = ? 168 LPP record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w)
169 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where
170 tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P
171 tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) )
172 (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where
173 tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1))
174 tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
177 FP : Filter LPP 175 FP : Filter LPP
178 FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 176 FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
179 uFP : ultra-filter FP 177 uFP : ultra-filter FP
180 uFP = record { proper = ? ; ultra = ? } 178 uFP = record { proper = ? ; ultra = ? }
181 LQ : HOD 179 LQ : HOD
182 LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) } 180 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
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 181 LQQ : LQ ⊆ Power Q
188 LQQ = ? 182 LQQ = ?
189 uflpp : UFLP {P} TP {LP} LPP FP uFP 183 uflpp : UFLP {P} TP {LP} LPP FP uFP
190 uflpp = ? 184 uflpp = record { limit = ? ; P∋limit = ? ; is-limit = ? }
191 185
192 186
193 187
194 188
195 189