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

comparison src/Topology.agda @ 1198:6e0cc71097e0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fip <-> compact done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 Mar 2023 09:00:11 +0900
parents 0a88fcd5d1c9
children 1338b6c6a9b6
comparison
equal deleted inserted replaced
1197:0a88fcd5d1c9 1198:6e0cc71097e0
281 281
282 data Finite-∪ (S : HOD) : Ordinal → Set n where 282 data Finite-∪ (S : HOD) : Ordinal → Set n where
283 fin-e : Finite-∪ S o∅ 283 fin-e : Finite-∪ S o∅
284 fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) 284 fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x ))
285 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) 285 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
286 -- Finite-∪ S y → Union y ⊆ S
286 287
287 record Compact {L : HOD} (top : Topology L) : Set n where 288 record Compact {L : HOD} (top : Topology L) : Set n where
288 field 289 field
289 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal 290 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
290 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L 291 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L
418 open _==_ 419 open _==_
419 420
420 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 421 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
421 Compact→FIP {L} top compact with trio< (& L) o∅ 422 Compact→FIP {L} top compact with trio< (& L) o∅
422 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 423 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
423 ... | tri≈ ¬a b ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX xx) } where 424 ... | tri≈ ¬a L=0 ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX fip xx) } where
424 fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ¬ odef (* X) x 425 -- empty L case
425 fip000 {X} {x} CX xx = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) b)) o∅≡od∅ ) (sym &iso) 426 -- if 0 < X then 0 < x ∧ L ∋ xfrom fip
426 ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) ? )) 427 -- if 0 ≡ X then ¬ odef X x
428 fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ({y : Ordinal} → Subbase (* X) y → o∅ o< y) → ¬ odef (* X) x
429 fip000 {X} {x} CX fip xx with trio< o∅ X
430 ... | tri< 0<X ¬b ¬c = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) L=0)) o∅≡od∅ ) (sym &iso)
431 ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) Xe )) where
432 0<x : o∅ o< x
433 0<x = fip (gi xx )
434 e : HOD -- we have an element of x
435 e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
436 Xe : odef (* x) (& e)
437 Xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
438 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
439 * X ≡⟨ cong (*) (sym 0=X) ⟩
440 * o∅ ≡⟨ o∅≡od∅ ⟩
441 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
442 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
427 -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) )) 443 -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) ))
428 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where 444 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
429 -- set of coset of X 445 -- set of coset of X
430 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal 446 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
431 OX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) 447 OX {X} ox = & ( Replace (* X) (λ z → L ＼ z ))
438 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) 454 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
439 -- it means there is a limit 455 -- it means there is a limit
440 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 456 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
441 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) 457 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ )
442 has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where 458 has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where
443 fp07 : HOD -- we have an element of X 459 e : HOD -- we have an element of X
444 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 460 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
445 fp08 : odef (* X) (& fp07) 461 Xe : odef (* X) (& e)
446 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 462 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
447 no-cover : ¬ ( (* (OX CX)) covers L ) 463 no-cover : ¬ ( (* (OX CX)) covers L )
448 no-cover cov = ⊥-elim (f20 (Compact.isCover compact (OOX CX) cov)) where 464 no-cover cov = ⊥-elim (no-finite-cover (Compact.isCover compact (OOX CX) cov)) where
465 -- construct Subase from Finite-∪
449 fp01 : Ordinal 466 fp01 : Ordinal
450 fp01 = Compact.finCover compact (OOX CX) cov 467 fp01 = Compact.finCover compact (OOX CX) cov
451 record SB (t : Ordinal) : Set n where 468 record SB (t : Ordinal) : Set n where
452 field 469 field
453 i : Ordinal 470 i : Ordinal
454 sb : Subbase (* X) (& (L ＼ * i)) 471 sb : Subbase (* X) (& (L ＼ * i))
455 not-t : (L ＼ * i) ⊆ (L ＼ Union ( * t ) ) 472 t⊆i : (L ＼ * i) ⊆ (L ＼ Union ( * t ) )
456 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t 473 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t
457 fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = fp23 } where 474 fp02 t fin-e = record { i = & ( L ＼ e) ; sb = gi (subst (λ k → odef (* X) k) fp21 Xe) ; t⊆i = fp23 } where
458 fp22 : fp07 ⊆ L 475 -- t ≡ o∅, no cover. Any subst of L is ok and we have e ⊆ L
459 fp22 {x} lt = cs⊆L top (CX fp08) lt 476 fp22 : e ⊆ L
460 fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07))) 477 fp22 {x} lt = cs⊆L top (CX Xe) lt
478 fp21 : & e ≡ & (L ＼ * (& (L ＼ e)))
461 fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso))) 479 fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso)))
462 fp23 : (L ＼ * (& (L ＼ fp07))) ⊆ (L ＼ Union (* o∅)) 480 fp23 : (L ＼ * (& (L ＼ e))) ⊆ (L ＼ Union (* o∅))
463 fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫ 481 fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫
464 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = fp24 } where 482 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; t⊆i = fp24 } where
483 -- we have a single cover x, L ＼ * x is single finite intersection
465 fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x)))) 484 fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x))))
466 fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25 ⟫ where 485 fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25 ⟫ where
467 fp25 : ¬ odef (Union (* x , * x)) y 486 fp25 : ¬ odef (Union (* x , * x)) y
468 fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) 487 fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
469 fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) 488 fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
470 fp03 : odef (* X) (& (L ＼ * x)) 489 fp03 : odef (* X) (& (L ＼ * x)) -- becase x is an element of Replace (* X) (λ z → L ＼ z )
471 fp03 with subst (λ k → odef k x ) *iso tx 490 fp03 with subst (λ k → odef k x ) *iso tx
472 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where 491 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
473 fip34 : * z1 ⊆ L 492 fip34 : * z1 ⊆ L
474 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 493 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
475 fip33 : z1 ≡ & (L ＼ * x) 494 fip33 : z1 ≡ & (L ＼ * x)
477 z1 ≡⟨ sym &iso ⟩ 496 z1 ≡⟨ sym &iso ⟩
478 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩ 497 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩
479 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ 498 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
480 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ 499 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
481 & (L ＼ * x ) ∎ where open ≡-Reasoning 500 & (L ＼ * x ) ∎ where open ≡-Reasoning
482 fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = fp35 } where 501 fp02 t (fin-∪ {tx} {ty} ux uy ) = record { i = & (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ; sb = fp11 ; t⊆i = fp35 } where
483 fp35 : (L ＼ * (& (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty)))) 502 fp35 : (L ＼ * (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty))))
484 fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36 where 503 fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36 where
485 fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z 504 fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z
486 fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) ao )) 505 fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) ao ))
487 fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) *iso uz) where 506 fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) *iso uz) where
488 fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z 507 fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z
491 fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } = 510 fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } =
492 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox ) 511 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox )
493 fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz 512 fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz
494 ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } 513 ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz }
495 ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } 514 ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz }
496 fp36 : (L ＼ (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* tx ∪ * ty)) 515 fp36 : (L ＼ (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* tx ∪ * ty))
497 fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where 516 fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where
498 fp37 : ¬ odef (Union (* tx ∪ * ty)) z 517 fp37 : ¬ odef (Union (* tx ∪ * ty)) z
499 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where 518 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
500 fp38 : (L ＼ (* (SB.i (fp02 tx x)))) ⊆ (L ＼ Union (* tx)) 519 fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx))
501 fp38 = SB.not-t (fp02 tx x) 520 fp38 = SB.t⊆i (fp02 tx ux)
502 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx x))) 521 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux)))
503 fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx x))} (fp40 x txw) 522 fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx ux))} (fp40 ux txw)
504 ... | case1 sb = sb 523 ... | case1 sb = sb
505 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) 524 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
506 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where 525 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
507 fp38 : (L ＼ (* (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* ty)) 526 fp38 : (L ＼ (* (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* ty))
508 fp38 = SB.not-t (fp02 ty y) 527 fp38 = SB.t⊆i (fp02 ty uy)
509 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty y))) 528 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy)))
510 fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty y))} (fp40 y tyw) 529 fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw)
511 ... | case1 sb = sb 530 ... | case1 sb = sb
512 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) 531 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw )
513 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) 532 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
514 fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where 533 fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
515 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x 534 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
520 fp06 (case2 ty) = ¬ty ty 539 fp06 (case2 ty) = ¬ty ty
521 fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x 540 fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x
522 fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt 541 fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt
523 ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) 542 ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso)
524 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ 543 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫
525 fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))))) 544 fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))))))
526 fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx x)) (SB.sb (fp02 ty y )) ) 545 fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx ux)) (SB.sb (fp02 ty uy )) )
527 fp12 : (L ＼ * (SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)))) ⊆ Union (* fp01) 546 --
528 fp12 {x} ⟪ Lx , not ⟫ = fp17 fp19 where 547 -- becase of fip, finite cover cannot be a cover
529 fcov = Compact.isCover compact (OOX CX) cov 548 --
530 fp13 : Ordinal
531 fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
532 fp16 : {y : Ordinal} → odef (L ＼ * fp13) y → odef L y
533 fp16 {y} ⟪ Ly , _ ⟫ = Ly
534 fp15 : ¬ ( odef (* fp13) x)
535 fp15 = not
536 fp19 : odef (L ＼ * fp13) x
537 fp19 with ∨L＼X {L} {* fp13} Lx
538 fp19 | case1 lt = ⊥-elim (not lt)
539 fp19 | case2 lt = lt
540 fp17 : (L ＼ * fp13 ) ⊆ Union (* fp01 )
541 fp17 {y} lt = record { owner = cover fcov (fp16 lt) ; ao = P∋cover fcov (fp16 lt) ; ox = isCover fcov (fp16 lt) }
542 fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov) 549 fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov)
543 fcov = Compact.isFinite compact (OOX CX) cov 550 fcov = Compact.isFinite compact (OOX CX) cov
544 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i) 551 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i)
545 0<sb {i} sb = fip sb 552 0<sb {i} sb = fip sb
546 sb : SB (Compact.finCover compact (OOX CX) cov) 553 sb : SB (Compact.finCover compact (OOX CX) cov)
547 sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) 554 sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov)
548 f20 : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) 555 no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L )
549 f20 fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where 556 no-finite-cover fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where
550 f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) 557 f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov)))
551 f23 = SB.not-t sb 558 f23 = SB.t⊆i sb
552 f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ 559 f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅
553 f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where 560 f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
554 f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x ) 561 f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x )
555 f24 {x} ⟪ Lx , not ⟫ = not record { owner = cover fcovers Lx ; ao = P∋cover fcovers Lx ; ox = isCover fcovers Lx } 562 f24 {x} ⟪ Lx , not ⟫ = not record { owner = cover fcovers Lx ; ao = P∋cover fcovers Lx ; ox = isCover fcovers Lx }
556 f25 : & od∅ o< (& (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ) 563 f25 : & od∅ o< (& (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) )
557 f25 = ordtrans<-≤ (subst (λ k → k o< & (L ＼ * (SB.i sb))) (sym ord-od∅) (0<sb (SB.sb sb) ) ) ( begin 564 f25 = ordtrans<-≤ (subst (λ k → k o< & (L ＼ * (SB.i sb))) (sym ord-od∅) (0<sb (SB.sb sb) ) ) ( begin
558 & (L ＼ * (SB.i sb)) ≤⟨ ⊆→o≤ f23 ⟩ 565 & (L ＼ * (SB.i sb)) ≤⟨ ⊆→o≤ f23 ⟩
559 & (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ∎ ) where open o≤-Reasoning O 566 & (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ∎ ) where open o≤-Reasoning O
560 567
561 record NC : Set n where -- x is not covered 568 record NC : Set n where -- find an element xi, which is not covered (which is a limit point)
562 field 569 field
563 x : Ordinal 570 x : Ordinal
564 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x 571 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x
565 not-covered : NC 572 not-covered : NC
566 not-covered with ODC.p∨¬p O NC 573 not-covered with ODC.p∨¬p O NC
592 fp05 : {y : Ordinal } → (Xy : odef (* X) y ) → odef ( * y) (NC.x not-covered ) 599 fp05 : {y : Ordinal } → (Xy : odef (* X) y ) → odef ( * y) (NC.x not-covered )
593 fp05 {y} Xy = NC.yx not-covered Xy 600 fp05 {y} Xy = NC.yx not-covered Xy
594 fp06 : NC.x not-covered o≤ & (* X) 601 fp06 : NC.x not-covered o≤ & (* X)
595 fp06 = begin 602 fp06 = begin
596 NC.x not-covered ≡⟨ sym &iso ⟩ 603 NC.x not-covered ≡⟨ sym &iso ⟩
597 & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ 604 & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered Xe)) ⟩
598 & fp07 <⟨ c<→o< fp08 ⟩ 605 & e <⟨ c<→o< Xe ⟩
599 & (* X) ∎ where open o≤-Reasoning O 606 & (* X) ∎ where open o≤-Reasoning O
600 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 607 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
601 → Ordinal 608 → Ordinal
602 limit {X} CX fip with trio< X o∅ 609 limit {X} CX fip with trio< X o∅
603 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 610 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )