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

comparison src/Topology.agda @ 1163:cd54ee498249

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 21 Jan 2023 09:02:52 +0900
parents 0a6040d914f8
children 5e065f0a7ba2
comparison
equal deleted inserted replaced
1162:0a6040d914f8 1163:cd54ee498249
64 P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1 64 P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1
65 , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos ⟫ 65 , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos ⟫
66 66
67 open Topology 67 open Topology
68 68
69 -- Closure ( Intersection of Closed Set which include A )
70
69 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD 71 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD
70 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } 72 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) }
71 ; odmax = & L ; <odmax = odef∧< } 73 ; odmax = & L ; <odmax = odef∧< }
72 74
73 ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L 75 ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L
74 ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic 76 ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic
75 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) 77 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
76 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) 78 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
77 79
80 -- Closure is Closed Set
81
78 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A 82 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A
79 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS) where 83 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS) where
80 OCl : HOD 84 OCl : HOD -- set of open set which it not contains A
81 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< } 85 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< }
82 OCl⊆OS : OCl ⊆ OS top 86 OCl⊆OS : OCl ⊆ OS top
83 OCl⊆OS ox = proj1 ox 87 OCl⊆OS ox = proj1 ox
84 UOCl-is-OS : OS top ∋ Union OCl 88 UOCl-is-OS : OS top ∋ Union OCl
85 UOCl-is-OS = o∪ top OCl⊆OS 89 UOCl-is-OS = o∪ top OCl⊆OS
98 cc07 : A ⊆ (L ＼ * (& (L ＼ * c))) 102 cc07 : A ⊆ (L ＼ * (& (L ＼ * c)))
99 cc07 {z} az = subst (λ k → odef k z ) ( 103 cc07 {z} az = subst (λ k → odef k z ) (
100 begin * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩ 104 begin * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩
101 L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩ 105 L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩
102 L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning 106 L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning
103 -- ksubst ( λ k → A ⊆ ( L ＼ k )) *iso (subst (λ k → A ⊆ k ) (L＼Lx=x ? ) (ac az) )
104 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x 107 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x
105 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where 108 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where
109 -- if x is in Cl A, it is in some c : CS, OCl says it is not , i.e. L ＼ o ∋ x, so it is in (L ＼ Union OCl) x
106 cc04 : ¬ odef (Union OCl) x 110 cc04 : ¬ odef (Union OCl) x
107 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where 111 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where
108 cc05 : odef (* (& (L ＼ * o))) x 112 cc05 : odef (* (& (L ＼ * o))) x
109 cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) (sym *iso) A⊆L-o) 113 cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) (sym *iso) A⊆L-o)
110 114
477 481
478 open import maximum-filter O 482 open import maximum-filter O
479 483
480 UFLP→FIP : {P : HOD} (TP : Topology P) → 484 UFLP→FIP : {P : HOD} (TP : Topology P) →
481 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP 485 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP
482 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where 486 UFLP→FIP {P} TP uflp with trio< (& P) o∅
487 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
488 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where
489 -- P is empty
490 fip02 : {x : Ordinal } → ¬ odef P x
491 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
492 ... | tri> ¬a ¬b 0<P = record { limit = uf00 ; is-limit = {!!} } where
483 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 493 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
484 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x 494 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
485 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD 495 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
486 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) 496 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
487 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } 497 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) }
532 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x 542 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
533 ufl01 = ? 543 ufl01 = ?
534 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v 544 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v
535 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ? 545 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?
536 546
547 FilterProduct : {P Q LP LQ : HOD }
548 → (LPP : LP ⊆ Power P) (FP : Filter {LP} LPP)
549 → (LPQ : LQ ⊆ Power Q) (FQ : Filter {LQ} LPQ)
550 → Filter {ZFP LP LQ} ?
551 FilterProduct = ?
552
553 FilterProj : {P Q LPQ : HOD }
554 → ( LPPQ : LPQ ⊆ Power (ZFP P Q))
555 → Filter {LPQ} LPPQ
556 → (Filter {Proj1PP LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2PP LPQ (Power P) (Power Q)} ?)
557 FilterProj = ?
558
559 ProuctLimit→ProjLimit : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)
560 → ( {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF )
561 → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TP LP F UF)
562 ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TQ LP F UF)
563 ProuctLimit→ProjLimit = ?
564
565 ProjLimit→ProductLimit : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)
566 → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TP LP F UF)
567 ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TQ LP F UF)
568 → {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF
569 ProjLimit→ProductLimit = ?
570
537 -- product topology of compact topology is compact 571 -- product topology of compact topology is compact
538 572
539 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) 573 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ)
540 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where 574 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
541 uflP : {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) 575 uflP : {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F)