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

comparison src/Topology.agda @ 482:ce4f3f180b8e

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 Wed, 06 Apr 2022 07:57:37 +0900
parents a5f8084b8368
children 7ce2cc622c92
comparison
equal deleted inserted replaced
481:263d2d1a000e 482:ce4f3f180b8e
30 import ODC 30 import ODC
31 open ODC O 31 open ODC O
32 32
33 open import filter 33 open import filter
34 34
35 record Toplogy ( L : HOD ) : Set (suc n) where 35 record Topology ( L : HOD ) : Set (suc n) where
36 field 36 field
37 OS : HOD 37 OS : HOD
38 OS⊆PL : OS ⊆ Power L 38 OS⊆PL : OS ⊆ Power L
39 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P 39 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P
40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) 40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
41 41
42 open Toplogy 42 open Topology
43 43
44 record _covers_ ( P q : HOD ) : Set (suc n) where 44 record _covers_ ( P q : HOD ) : Set (suc n) where
45 field 45 field
46 cover : {x : HOD} → q ∋ x → HOD 46 cover : {x : HOD} → q ∋ x → HOD
47 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt 47 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
56 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y) 56 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
57 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q) 57 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
58 58
59 -- Limit point 59 -- Limit point
60 60
61 record LP ( L S x : HOD ) (top : Toplogy L) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where 61 record LP ( L S x : HOD ) (top : Topology L) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
62 field 62 field
63 neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD 63 neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD
64 isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x ) 64 isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )
65 65
66 -- Finite Intersection Property 66 -- Finite Intersection Property
86 isFinCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y 86 isFinCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y
87 isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y ) 87 isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y )
88 88
89 -- FIP is Compact 89 -- FIP is Compact
90 90
91 FIP→Compact : {L P : HOD} → Tolopogy L → FIP L P → Compact L P 91 FIP→Compact : {L P : HOD} → Topology L → FIP L P → Compact L P
92 FIP→Compact = ? 92 FIP→Compact = {!!}
93 93
94 Compact→FIP : {L P : HOD} → Tolopogy L → Compact L P → FIP L P 94 Compact→FIP : {L P : HOD} → Topology L → Compact L P → FIP L P
95 Compact→FIP = ? 95 Compact→FIP = {!!}
96 96
97 -- Product Topology 97 -- Product Topology
98 98
99 _Top⊗_ : {P Q : HOD} → Topology P → Tolopogy Q → Topology ( P ⊗ Q ) 99 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology {!!}
100 _Top⊗_ = ? 100 _Top⊗_ = {!!}
101 101
102 -- existence of Ultra Filter 102 -- existence of Ultra Filter
103 103
104 -- Ultra Filter has limit point 104 -- Ultra Filter has limit point
105 105