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

comparison src/Topology.agda @ 431:a5f8084b8368

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganiztion for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 10:23:37 +0900
parents
children ce4f3f180b8e
comparison
equal deleted inserted replaced
430:28c7be8f252c 431:a5f8084b8368
1 open import Level
2 open import Ordinals
3 module Topology {n : Level } (O : Ordinals {n}) where
4
5 open import zf
6 open import logic
7 open _∧_
8 open _∨_
9 open Bool
10
11 import OD
12 open import Relation.Nullary
13 open import Data.Empty
14 open import Relation.Binary.Core
15 open import Relation.Binary.PropositionalEquality
16 import BAlgbra
17 open BAlgbra O
18 open inOrdinal O
19 open OD O
20 open OD.OD
21 open ODAxiom odAxiom
22 import OrdUtil
23 import ODUtil
24 open Ordinals.Ordinals O
25 open Ordinals.IsOrdinals isOrdinal
26 open Ordinals.IsNext isNext
27 open OrdUtil O
28 open ODUtil O
29
30 import ODC
31 open ODC O
32
33 open import filter
34
35 record Toplogy ( L : HOD ) : Set (suc n) where
36 field
37 OS : HOD
38 OS⊆PL : OS ⊆ Power L
39 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P
40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
41
42 open Toplogy
43
44 record _covers_ ( P q : HOD ) : Set (suc n) where
45 field
46 cover : {x : HOD} → q ∋ x → HOD
47 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
48 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
49
50 -- Base
51 -- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
52 -- W ⊆ U ∩ V and x ∈ W .
53
54 data genTop (P : HOD) : HOD → Set (suc n) where
55 gi : {x : HOD} → P ∋ x → genTop P x
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)
58
59 -- Limit point
60
61 record LP ( L S x : HOD ) (top : Toplogy L) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
62 field
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 )
65
66 -- Finite Intersection Property
67
68 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
69 fin-∩e : {x : HOD} → S ∋ x → Finite-∩ S x
70 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
71
72 record FIP ( L P : HOD ) : Set (suc n) where
73 field
74 fipS⊆PL : P ⊆ Power L
75 fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )
76
77 -- Compact
78
79 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
80 fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x
81 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
82
83 record Compact ( L P : HOD ) : Set (suc n) where
84 field
85 finCover : {X y : HOD} → X covers P → P ∋ y → HOD
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 )
88
89 -- FIP is Compact
90
91 FIP→Compact : {L P : HOD} → Tolopogy L → FIP L P → Compact L P
92 FIP→Compact = ?
93
94 Compact→FIP : {L P : HOD} → Tolopogy L → Compact L P → FIP L P
95 Compact→FIP = ?
96
97 -- Product Topology
98
99 _Top⊗_ : {P Q : HOD} → Topology P → Tolopogy Q → Topology ( P ⊗ Q )
100 _Top⊗_ = ?
101
102 -- existence of Ultra Filter
103
104 -- Ultra Filter has limit point
105
106 -- FIP is UFL
107
108 -- Product of UFL has limit point (Tychonoff)
109