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

comparison Topology.agda @ 428:94392feeebc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Topology
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 19 Dec 2020 21:43:21 +0900
parents
children 8d8149bcd4d1
comparison
equal deleted inserted replaced
427:9b0630f03c4b 428:94392feeebc5
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 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
73 fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x
74 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
75
76 record FIP ( L : HOD ) : Set (suc n) where
77 field
78 fipS : HOD
79 fipS⊆PL : fipS ⊆ Power L
80 fip≠φ : { x : HOD } → Finite-∩ fipS x → ¬ ( x ≡ od∅ )
81
82 -- Compact
83
84 record Compact ( L P : HOD ) : Set (suc n) where
85 field
86 finCover : {X y : HOD} → X covers P → P ∋ y → HOD
87 isFinCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y
88 isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y )
89
90
91 -- Product Topology