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

comparison src/Topology.agda @ 1120:e086a266c6b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIP fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2023 09:28:23 +0900
parents 5b0525cb9a5d
children 98af35c9711f
comparison
equal deleted inserted replaced
1119:5b0525cb9a5d 1120:e086a266c6b7
139 tp06 : * b ⊆ Union q 139 tp06 : * b ⊆ Union q
140 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } 140 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz }
141 141
142 -- covers 142 -- covers
143 143
144 record _covers_ ( P q : HOD ) : Set (suc n) where 144 record _covers_ ( P q : HOD ) : Set n where
145 field 145 field
146 cover : {x : HOD} → q ∋ x → HOD 146 cover : {x : Ordinal } → odef q x → Ordinal
147 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt 147 P∋cover : {x : Ordinal } → {lt : odef q x} → odef P (cover lt)
148 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x 148 isCover : {x : Ordinal } → {lt : odef q x} → odef (* (cover lt)) x
149
150 open _covers_
149 151
150 -- Finite Intersection Property 152 -- Finite Intersection Property
151 153
152 record FIP {L : HOD} (top : Topology L) : Set (suc n) where 154 record FIP {L : HOD} (top : Topology L) : Set n where
153 field 155 field
154 fip≠φ : { C : HOD } { x : Ordinal } → C ⊆ CS top → Subbase C x → o∅ o< x 156 finite : {X : Ordinal } → * X ⊆ CS top
157 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal
158 limit : {X : Ordinal } → (CX : * X ⊆ CS top )
159 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x )
160 → {x : Ordinal } → odef (* X) x → odef (* x) (finite CX fip)
155 161
156 -- Compact 162 -- Compact
157 163
158 data Finite-∪ (S : HOD) : Ordinal → Set n where 164 data Finite-∪ (S : HOD) : Ordinal → Set n where
159 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x 165 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x
160 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) 166 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
161 167
162 record Compact {L : HOD} (top : Topology L) : Set (suc n) where 168 record Compact {L : HOD} (top : Topology L) : Set n where
163 field 169 field
164 finCover : {X : HOD} → X ⊆ OS top → X covers L → HOD 170 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
165 isCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L 171 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L
166 isFinite : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (& (finCover xo xcp ) ) 172 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp )
167 173
168 -- FIP is Compact 174 -- FIP is Compact
169 175
170 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top 176 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top
171 FIP→Compact {L} top fip = record { finCover = finCover ; isCover = ? ; isFinite = ? } where 177 FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
172 finCover : {C : HOD} → C ⊆ OS top → C covers L → HOD 178 remain : {X : Ordinal } → (* X) ⊆ OS top → ¬ ( (* X) covers L ) → Ordinal
173 finCover {C} C<T CL = record { od = record { def = λ x → odef L x ∧ ( ¬ Subbase C x) } ; odmax = & L ; <odmax = odef∧< } 179 remain = ?
174 isConver : {C : HOD} (xo : C ⊆ OS top) (xcp : C covers L) → (finCover xo xcp) covers L 180 remain-is-intersection : {X : Ordinal } → (ox : (* X) ⊆ OS top) → (r : ¬ ( (* X) covers L ) )
175 isConver {C} xo xcp = record { cover = λ lx → ? ; P∋cover = ? ; isCover = ? } 181 → {x : Ordinal } → odef (* X) x → odef (L ＼ * x ) (remain ox r)
182 -- HOD of a counter example of fip
183 tp00 : {X : Ordinal} → * X ⊆ OS top → HOD
184 tp00 {X} ox = record { od = record { def = λ x → { C : Ordinal } → * C ⊆ * X → Subbase (L ＼ * C) x }
185 ; odmax = & L ; <odmax = ? }
186 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
187 finCover {X} ox oc = ? where
188 -- X is the counter example of fip
189 tp01 : {x : Ordinal } → odef (L ＼ * X) ( FIP.finite fip ? ? ) → odef (* x) ( FIP.finite fip ? ? )
190 tp01 {x} P = FIP.limit fip ? ? ?
191 -- yes, it is finite
192 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
193 isFinite = ?
194 -- is also a cover
195 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
196 isCover1 = ?
197
176 198
177 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 199 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
178 Compact→FIP = {!!} 200 Compact→FIP = {!!}
179 201
180 -- Product Topology 202 -- Product Topology