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

comparison src/Topology.agda @ 1486:49c3ef1e9b4f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Topology fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jul 2024 16:07:57 +0900
parents 5dacb669f13b
children
comparison
equal deleted inserted replaced
1485:5dacb669f13b 1486:49c3ef1e9b4f
596 fp37 : ¬ odef (Union (* tx ∪ * ty)) z 596 fp37 : ¬ odef (Union (* tx ∪ * ty)) z
597 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where 597 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
598 fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx)) 598 fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx))
599 fp38 = SB.t⊆i (fp02 tx ux) 599 fp38 = SB.t⊆i (fp02 tx ux)
600 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux))) 600 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux)))
601 fp39 {w} txw with ∨L＼X {L} {(SB.i (fp02 tx ux))} (fp40 ux ?) 601 fp39 {w} txw with ∨L＼X {* (SB.i (fp02 tx ux))} (fp40 ux txw)
602 ... | t = ? 602 ... | case1 sb = sb
603 -- ... | case1 sb = sb 603 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
604 -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
605 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where 604 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
606 fp38 : (L ＼ (* (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* ty)) 605 fp38 : (L ＼ (* (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* ty))
607 fp38 = SB.t⊆i (fp02 ty uy) 606 fp38 = SB.t⊆i (fp02 ty uy)
608 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy))) 607 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy)))
609 fp39 {w} tyw = ? -- with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw) 608 fp39 {w} tyw with ∨L＼X {* (SB.i (fp02 ty uy))} (fp40 uy tyw)
610 -- ... | case1 sb = sb 609 ... | case1 sb = sb
611 -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) 610 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw )
612 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) 611 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
613 fp04 {tx} {ty} = ==→o≡ record { eq→ = fp05 ; eq← = fp09 } where 612 fp04 {tx} {ty} = ==→o≡ record { eq→ = fp05 ; eq← = fp09 } where
614 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x 613 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
615 fp05 {x} lt with eq← *iso∩ lt 614 fp05 {x} lt with eq← *iso∩ lt
616 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = eq→ (＼-cong L L (* tx ∪ * ty) (* (& (* tx ∪ * ty))) ==-refl (==-sym *iso) ) ⟪ Lx , fp06 ⟫ where 615 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = eq→ (＼-cong L L (* tx ∪ * ty) (* (& (* tx ∪ * ty))) ==-refl (==-sym *iso) ) ⟪ Lx , fp06 ⟫ where
631 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i) 630 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i)
632 0<sb {i} sb = fip sb 631 0<sb {i} sb = fip sb
633 sb : SB (Compact.finCover compact (OOX CX) cov) 632 sb : SB (Compact.finCover compact (OOX CX) cov)
634 sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) 633 sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov)
635 no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) 634 no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L )
636 no-finite-cover fcovers = ? where -- ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where 635 no-finite-cover fcovers = ⊥-elim ( o<¬≡ (sym (==→o≡ f22)) f25 ) where
637 f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) 636 f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov)))
638 f23 = SB.t⊆i sb 637 f23 = SB.t⊆i sb
639 f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ 638 f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅
640 f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where 639 f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
641 f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x ) 640 f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x )
653 coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X 652 coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X
654 ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) } 653 ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) }
655 fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ ) 654 fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ )
656 fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where 655 fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where
657 fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x 656 fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x
658 fp19 {y} Xy = ? -- with ∨L＼X {L} {* y} {x} Lx 657 fp19 {y} Xy with ∨L＼X {* y} {x} Lx
659 -- ... | case1 yx = yx 658 ... | case1 yx = yx
660 -- ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where 659 ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where
661 -- fp20 : odef (* X) y ∧ odef (L ＼ * y) x 660 fp20 : odef (* X) y ∧ odef (L ＼ * y) x
662 -- fp20 = ⟪ Xy , lyx ⟫ 661 fp20 = ⟪ Xy , lyx ⟫
663 coverf : {x : Ordinal} → (Lx : odef L x ) → HOD 662 coverf : {x : Ordinal} → (Lx : odef L x ) → HOD
664 coverf Lx = minimal (coverSet Lx) (fp17 Lx) 663 coverf Lx = minimal (coverSet Lx) (fp17 Lx)
665 fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt)) 664 fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt))
666 fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) ? record { z = _ ; az = fp25 ; x=ψz = fp24 } where 665 fp22 {x} Lx = eq← *iso record { z = _ ; az = fp25 ; x=ψz = fp24 } where
667 fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx))) 666 fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx)))
668 fp24 = cong (λ k → & ( L ＼ k )) ? 667 fp24 = ==→o≡ (＼-cong L L (coverf Lx) (* (& (coverf Lx))) ==-refl (==-sym *iso) )
669 fp25 : odef (* X) (& (coverf Lx)) 668 fp25 : odef (* X) (& (coverf Lx))
670 fp25 = proj1 ( x∋minimal (coverSet Lx) (fp17 Lx) ) 669 fp25 = proj1 ( x∋minimal (coverSet Lx) (fp17 Lx) )
671 fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x 670 fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x
672 fp23 {x} Lx = subst (λ k → odef k x) ? ⟪ Lx , fp26 ⟫ where 671 fp23 {x} Lx = eq← *iso ⟪ Lx , fp26 ⟫ where
673 fp26 : ¬ odef (coverf Lx) x 672 fp26 : ¬ odef (coverf Lx) x
674 fp26 = subst (λ k → ¬ odef k x ) ? (proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) )) ) 673 fp26 llx = proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) )) (eq← *iso llx)
675 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal 674 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal
676 limit {X} CX fip with trio< X o∅ 675 limit {X} CX fip with trio< X o∅
677 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 676 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
678 ... | tri≈ ¬a b ¬c = o∅ 677 ... | tri≈ ¬a b ¬c = o∅
679 ... | tri> ¬a ¬b c = NC.x ( has-intersection CX fip c) 678 ... | tri> ¬a ¬b c = NC.x ( has-intersection CX fip c)
710 NF⊆PP : NF ⊆ Power P 709 NF⊆PP : NF ⊆ Power P
711 NF⊆PP = nf00 710 NF⊆PP = nf00
712 f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q 711 f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q
713 f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where 712 f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where
714 f11 : * (Neighbor.u Np) ⊆ * (& q) 713 f11 : * (Neighbor.u Np) ⊆ * (& q)
715 f11 {x} ux = subst (λ k → odef k x ) ? ( p⊆q (subst (λ k → odef k x) ? (Neighbor.u⊆v Np ux)) ) 714 f11 {x} ux = eq← *iso ( p⊆q (eq→ *iso (Neighbor.u⊆v Np ux)) )
716 f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q) 715 f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q)
717 f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where 716 f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where
718 upq : Ordinal 717 upq : Ordinal
719 upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) ) 718 upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) )
720 ou : odef (OS TP) upq 719 ou : odef (OS TP) upq
721 ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq)) 720 ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq))
722 ux : odef (* upq) x 721 ux : odef (* upq) x
723 ux = subst ( λ k → odef k x ) ? ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ 722 ux = eq← *iso ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫
724 f20 : * upq ⊆ * (& (p ∩ q)) 723 f20 : * upq ⊆ * (& (p ∩ q))
725 f20 = subst₂ (λ j k → j ⊆ k ) ? ? ( λ {x} pq 724 f20 {x} lt = eq← *iso ⟪ eq→ *iso (Neighbor.u⊆v Np (proj1 pq)) , eq→ *iso (Neighbor.u⊆v Nq (proj2 pq)) ⟫ where
726 → ⟪ subst (λ k → odef k x) ? (Neighbor.u⊆v Np (proj1 pq)) , subst (λ k → odef k x) ? (Neighbor.u⊆v Nq (proj2 pq)) ⟫ ) 725 pq : odef (* (Neighbor.u Np) ∩ * (Neighbor.u Nq)) x
726 pq = eq→ *iso lt
727 727
728 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q) 728 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
729 CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) ? pqx 729 CAP P {p} {q} Pp Pq x pqx with eq→ *iso pqx
730 ... | t = ? 730 ... | ⟪ px , qx ⟫ = Pp _ (eq← *iso px )
731 -- ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) ? px )
732 731
733 NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p ) 732 NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p )
734 NEG P {p} Pp x vx with subst (λ k → odef k x) ? vx 733 NEG P {p} Pp x vx with eq→ *iso vx
735 ... | t = ? 734 ... | ⟪ Px , npx ⟫ = Px
736 -- ... | ⟪ Px , npx ⟫ = Px 735
737 736
738 737
739