Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/Topology.agda @ 1104:81b859b678a8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Dec 2022 14:42:28 +0900 |
parents | a9a7ad7784cc |
children | fabcb7d9f50c |
line wrap: on
line diff
--- a/src/Topology.agda Thu Dec 29 10:58:42 2022 +0900 +++ b/src/Topology.agda Thu Dec 29 14:42:28 2022 +0900 @@ -65,13 +65,6 @@ g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y) g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q) --- Limit point - -record LP { L : HOD} (top : Topology L) ( S x : HOD ) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where - field - neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD - isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x ) - -- Finite Intersection Property data Finite-∩ (S : HOD) : HOD → Set (suc n) where @@ -166,9 +159,35 @@ Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where - uflp : {L : HOD} (LP : L ⊆ Power (ZFP P Q)) (F : Filter LP) - (uf : ultra-filter {L} {_} {LP} F) → UFLP (TP Top⊗ TQ) LP F uf - uflp {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } + uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) + (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf + uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where + lprod : {x y : Ordinal } → (ly : odef L y) → odef (ZFP P Q) x + lprod {x} {y} ly = LPQ ly x ? + -- LP : HOD + -- LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) + LP : HOD + LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) } + ; odmax = & P ; <odmax = ? } where + L→P : {y : Ordinal } → odef L y → HOD + L→P {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ1 (LPQ ly z yz ) ≡ x } + ; odmax = & P ; <odmax = ? } + LPP : LP ⊆ Power P + LPP = ? + FP : Filter LPP + FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } + uFP : ultra-filter FP + uFP = record { proper = ? ; ultra = ? } + LQ : HOD + LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) } + ; odmax = & P ; <odmax = ? } where + L→Q : {y : Ordinal } → odef L y → HOD + L→Q {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ2 (LPQ ly z yz ) ≡ x } + ; odmax = & Q ; <odmax = ? } + LQQ : LQ ⊆ Power Q + LQQ = ? + uflpp : UFLP {P} TP {LP} LPP FP uFP + uflpp = ?