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

comparison src/Topology.agda @ 1151:8a071bf52407

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finite intersection property to Compact done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 18 Jan 2023 01:43:24 +0900
parents fe0129c40745
children e1c6719a8c38
comparison
equal deleted inserted replaced
1150:fe0129c40745 1151:8a071bf52407
279 record CFIP (X x : Ordinal) : Set n where 279 record CFIP (X x : Ordinal) : Set n where
280 field 280 field
281 is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z) 281 is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z)
282 sx : Subbase (* x) o∅ 282 sx : Subbase (* x) o∅
283 Cex : (X : Ordinal ) → HOD 283 Cex : (X : Ordinal ) → HOD
284 Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L ＼ z))) ; <odmax = ? } where 284 Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L ＼ z))) ; <odmax = fip05 } where
285 fip05 : {y : Ordinal} → CFIP X y → y o< osuc (& L) 285 fip05 : {y : Ordinal} → CFIP X y → y o< osuc (& (Replace' (* X) (λ z xz → L ＼ z)))
286 fip05 {y} cf = subst₂ (λ j k → j o≤ k ) ? ? ( ⊆→o≤ ( CFIP.is-CS cf )) 286 fip05 {y} cf = subst₂ (λ j k → j o< osuc k ) &iso refl ( ⊆→o≤ ( CFIP.is-CS cf ) )
287 fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ ) 287 fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ )
288 fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where 288 fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
289 -- CX is finite intersection 289 -- CX is finite intersection
290 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 290 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
291 fip02 {C} {x} C<CX sc with trio< x o∅ 291 fip02 {C} {x} C<CX sc with trio< x o∅
319 -- create Finite-∪ from cex 319 -- create Finite-∪ from cex
320 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) 320 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
321 isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where 321 isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where
322 fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z ))) 322 fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z )))
323 fip30 x y x⊆cs (gi sb) = fip31 where 323 fip30 x y x⊆cs (gi sb) = fip31 where
324 fip32 : Replace' (* x) (λ z xz → L ＼ z) ⊆ * X -- x⊆cs :* x ⊆ Replace' (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
325 fip32 {w} record { z = z ; az = xz ; x=ψz = x=ψz } with x⊆cs xz
326 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
327 fip34 : * z1 ⊆ L
328 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
329 fip33 : z1 ≡ w
330 fip33 = begin
331 z1 ≡⟨ sym &iso ⟩
332 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩
333 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
334 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
335 & (L ＼ * z) ≡⟨ sym x=ψz ⟩
336 w ∎ where open ≡-Reasoning
324 fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z))) 337 fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z)))
325 fip31 = fin-e ? 338 fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
326 fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = ? 339 fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
340 fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L ＼ z₁)))
341 fip35 = subst (λ k → Finite-∪ (* X) k)
342 (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _ x⊆cs sy) (fip30 _ _ x⊆cs sz) )
327 -- is also a cover 343 -- is also a cover
328 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L 344 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
329 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) ? ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where 345 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
346 ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
330 -- record { cover = λ {x} Lx → ? ; P∋cover = ? ; isCover = ? } 347 -- record { cover = λ {x} Lx → ? ; P∋cover = ? ; isCover = ? }
348 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b))
349 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
350 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫
351 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫
352 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
353 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where
354 fip44 : {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal
355 fip44 {x} Lab with fip45 {L} {a} {b} Lab
356 ... | case1 La = cover ca La
357 ... | case2 Lb = cover cb Lb
358 fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt)
359 fip46 {x} Lab with fip45 {L} {a} {b} Lab
360 ... | case1 La = P∋cover ca La
361 ... | case2 Lb = P∋cover cb Lb
362 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x
363 fip47 {x} Lab with fip45 {L} {a} {b} Lab
364 ... | case1 La = isCover ca La
365 ... | case2 Lb = isCover cb Lb
331 fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y 366 fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y
332 → (Replace' (* x) (λ z xz → L ＼ z )) covers (L ＼ * y ) 367 → (Replace' (* x) (λ z xz → L ＼ z )) covers (L ＼ * y )
333 fip40 = ? 368 fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
369 ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where
370 fip41 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * a)
371 fip41 = fip40 x a x⊆r sa
372 fip42 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * b)
373 fip42 = fip40 x b x⊆r sb
374 fip40 x y x⊆r (gi sb) with x⊆r sb
375 ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
376 fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal
377 fip51 {w} Lyw = z
378 fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z
379 fip52 {w} Lyw = az
380 fip55 : * z ⊆ L
381 fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1
382 fip56 : * z ≡ L ＼ * y
383 fip56 = begin
384 * z ≡⟨ sym (L＼Lx=x fip55 ) ⟩
385 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso) ⟩
386 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz) ⟩
387 L ＼ * y ∎ where open ≡-Reasoning
388 fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z
389 fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
390 fip54 : z ≡ & ( L ＼ * y )
391 fip54 = begin
392 z ≡⟨ sym &iso ⟩
393 & (* z) ≡⟨ cong (&) fip56 ⟩
394 & (L ＼ * y )
395 ∎ where open ≡-Reasoning
396 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
397 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
398
334 399
335 400
336 -- some day 401 -- some day
337 Compact→FIP : Set (suc n) 402 Compact→FIP : Set (suc n)
338 Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top → FIP top 403 Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top → FIP top