Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1192:2c35ccd5aadd
...
| author | kono |
|---|---|
| date | Mon, 27 Feb 2023 13:13:15 +0800 |
| parents | d969fc17d049 |
| children |
| rev | line source |
|---|---|
| 1170 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 | |
| 431 | 3 open import Level |
| 4 open import Ordinals | |
| 5 module Topology {n : Level } (O : Ordinals {n}) where | |
| 6 | |
| 7 open import zf | |
| 8 open import logic | |
| 9 open _∧_ | |
| 10 open _∨_ | |
| 11 open Bool | |
| 12 | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
13 import OD |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
14 open import Relation.Nullary |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
15 open import Data.Empty |
| 431 | 16 open import Relation.Binary.Core |
| 1143 | 17 open import Relation.Binary.Definitions |
| 431 | 18 open import Relation.Binary.PropositionalEquality |
| 1124 | 19 import BAlgebra |
| 20 open BAlgebra O | |
| 431 | 21 open inOrdinal O |
| 22 open OD O | |
| 23 open OD.OD | |
| 24 open ODAxiom odAxiom | |
| 25 import OrdUtil | |
| 26 import ODUtil | |
| 27 open Ordinals.Ordinals O | |
| 28 open Ordinals.IsOrdinals isOrdinal | |
| 29 open Ordinals.IsNext isNext | |
| 30 open OrdUtil O | |
| 31 open ODUtil O | |
| 32 | |
| 33 import ODC | |
| 34 open ODC O | |
| 35 | |
| 1102 | 36 open import filter O |
| 1101 | 37 open import OPair O |
| 38 | |
| 482 | 39 record Topology ( L : HOD ) : Set (suc n) where |
| 431 | 40 field |
| 41 OS : HOD | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
42 OS⊆PL : OS ⊆ Power L |
|
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
43 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) |
| 1161 | 44 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P |
| 1122 | 45 OS∋od∅ : OS ∋ od∅ |
| 1160 | 46 --- we may add |
| 47 -- OS∋L : OS ∋ L | |
| 1101 | 48 -- closed Set |
| 49 CS : HOD | |
| 1119 | 50 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
| 51 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L ＼ * y)) → y o< osuc (& L) | |
| 52 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx )) | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
53 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
| 1108 | 54 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
| 1122 | 55 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L |
| 56 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) | |
| 57 CS∋L : CS ∋ L | |
| 1123 | 58 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where |
| 59 lem0 : L ＼ * (& L) ≡ od∅ | |
| 60 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0 | |
| 1154 | 61 CS⊆PL : CS ⊆ Power L |
| 1161 | 62 CS⊆PL {x} Cx y xy = proj1 Cx xy |
| 1160 | 63 P＼CS=OS : {cs : HOD} → CS ∋ cs → OS ∋ ( L ＼ cs ) |
| 64 P＼CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (cong (λ k → & ( L ＼ k)) *iso) olcs | |
| 65 P＼OS=CS : {cs : HOD} → OS ∋ cs → CS ∋ ( L ＼ cs ) | |
| 1161 | 66 P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1 |
| 1160 | 67 , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos ⟫ |
| 431 | 68 |
| 482 | 69 open Topology |
| 431 | 70 |
| 1163 | 71 -- Closure ( Intersection of Closed Set which include A ) |
| 72 | |
| 1162 | 73 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD |
| 74 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } | |
| 1150 | 75 ; odmax = & L ; <odmax = odef∧< } |
| 1122 | 76 |
| 1162 | 77 ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L |
| 78 ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic | |
| 1142 | 79 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) |
| 80 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) | |
| 1123 | 81 |
| 1163 | 82 -- Closure is Closed Set |
| 83 | |
| 1162 | 84 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A |
| 85 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS) where | |
| 1163 | 86 OCl : HOD -- set of open set which it not contains A |
| 1162 | 87 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< } |
| 88 OCl⊆OS : OCl ⊆ OS top | |
| 89 OCl⊆OS ox = proj1 ox | |
| 90 UOCl-is-OS : OS top ∋ Union OCl | |
| 91 UOCl-is-OS = o∪ top OCl⊆OS | |
| 92 cc00 : (L ＼ Union OCl) =h= Cl top A | |
| 93 cc00 = record { eq→ = cc01 ; eq← = cc03 } where | |
| 94 cc01 : {x : Ordinal} → odef (L ＼ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) | |
| 95 cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where | |
| 96 cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x → odef (* c) x | |
| 97 cc02 c cc ac nox with ODC.∋-p O (* c) (* x) | |
| 98 ... | yes y = subst (λ k → odef (* c) k) &iso y | |
| 99 ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) (sym *iso) cc06 } ) where | |
| 100 cc06 : odef (L ＼ * c) x | |
| 101 cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫ | |
| 102 cc08 : * c ⊆ L | |
| 103 cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc ) | |
| 104 cc07 : A ⊆ (L ＼ * (& (L ＼ * c))) | |
| 105 cc07 {z} az = subst (λ k → odef k z ) ( | |
| 106 begin * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩ | |
| 107 L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩ | |
| 108 L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning | |
| 109 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x | |
| 110 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where | |
| 1163 | 111 -- 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 |
| 1162 | 112 cc04 : ¬ odef (Union OCl) x |
| 113 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where | |
| 114 cc05 : odef (* (& (L ＼ * o))) x | |
| 115 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) | |
| 1161 | 116 |
| 1160 | 117 |
| 1119 | 118 -- Subbase P |
| 119 -- A set of countable intersection of P will be a base (x ix an element of the base) | |
| 1107 | 120 |
| 121 data Subbase (P : HOD) : Ordinal → Set n where | |
| 122 gi : {x : Ordinal } → odef P x → Subbase P x | |
| 123 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
| 124 | |
| 1119 | 125 -- |
| 1150 | 126 -- if y is in a Subbase, some element of P contains it |
| 1119 | 127 |
| 1111 | 128 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
| 129 sbp P {x} (gi {y} px) = x | |
| 130 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
| 1107 | 131 |
| 1111 | 132 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
| 133 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
134 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
| 1107 | 135 |
| 1155 | 136 sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x |
| 137 sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px) | |
| 138 sb⊆ {P} {Q} P⊆Q (g∩ px qx) = g∩ (sb⊆ P⊆Q px) (sb⊆ P⊆Q qx) | |
| 139 | |
| 1119 | 140 -- An open set generate from a base |
| 141 -- | |
| 1161 | 142 -- OS = { U ⊆ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊆ U } |
| 1114 | 143 |
| 1115 | 144 record Base (L P : HOD) (u x : Ordinal) : Set n where |
| 1114 | 145 field |
| 1150 | 146 b : Ordinal |
| 1161 | 147 u⊆L : * u ⊆ L |
| 1114 | 148 sb : Subbase P b |
| 149 b⊆u : * b ⊆ * u | |
| 150 bx : odef (* b) x | |
| 1150 | 151 x⊆L : odef L x |
| 1161 | 152 x⊆L = u⊆L (b⊆u bx) |
| 1114 | 153 |
| 1115 | 154 SO : (L P : HOD) → HOD |
| 1119 | 155 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where |
| 156 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | |
| 1150 | 157 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) |
| 1114 | 158 |
| 1111 | 159 record IsSubBase (L P : HOD) : Set (suc n) where |
| 1110 | 160 field |
| 1122 | 161 P⊆PL : P ⊆ Power L |
| 1116 | 162 -- we may need these if OS ∋ L is necessary |
| 163 -- p : {x : HOD} → L ∋ x → HOD | |
| 1161 | 164 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx |
| 1116 | 165 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x |
| 1110 | 166 |
| 1152 | 167 InducedTopology : (L P : HOD) → IsSubBase L P → Topology L |
| 168 InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00 | |
| 1122 | 169 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where |
| 170 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x | |
| 1150 | 171 tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) |
| 1115 | 172 tp00 : SO L P ⊆ Power L |
| 173 tp00 {u} ou x ux with ou ux | |
| 1161 | 174 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊆L (b⊆u bx) |
| 1115 | 175 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
| 1161 | 176 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊆L = subst (λ k → k ⊆ L) (sym *iso) ul |
| 1116 | 177 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
| 1115 | 178 px : odef (* (& p)) x |
| 179 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
| 180 qx : odef (* (& q)) x | |
| 181 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
| 182 b : Ordinal | |
| 183 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
| 1116 | 184 tp08 : * b ⊆ * (& (p ∩ q) ) |
| 1150 | 185 tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where |
| 1116 | 186 tp11 : * (Base.b (op px)) ⊆ * (& p ) |
| 187 tp11 = Base.b⊆u (op px) | |
| 188 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
| 189 tp12 = Base.b⊆u (oq qx) | |
| 1150 | 190 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p |
| 1116 | 191 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) |
| 1150 | 192 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q |
| 1116 | 193 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) |
| 194 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | |
| 195 tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ | |
|
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
196 ul : (p ∩ q) ⊆ L |
| 1161 | 197 ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq → (Base.u⊆L (op px)) (pz pq) ) where |
| 1116 | 198 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
| 199 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | |
| 1161 | 200 tp02 : { q : HOD} → q ⊆ SO L P → SO L P ∋ Union q |
| 201 tp02 {q} q⊆O {x} ux with subst (λ k → odef k x) *iso ux | |
| 202 ... | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx | |
| 203 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊆L = subst (λ k → k ⊆ L) (sym *iso) tp04 | |
| 1116 | 204 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where |
| 205 tp05 : Union q ⊆ L | |
| 1161 | 206 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx |
| 207 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
| 1116 | 208 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) |
|
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
209 tp04 : Union q ⊆ L |
| 1150 | 210 tp04 = tp05 |
| 1116 | 211 tp06 : * b ⊆ Union q |
| 1150 | 212 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } |
| 1110 | 213 |
| 1142 | 214 -- Product Topology |
| 215 | |
| 216 open ZFProduct | |
| 217 | |
| 1150 | 218 -- Product Topology is not |
| 1142 | 219 -- ZFP (OS TP) (OS TQ) (box) |
| 220 | |
| 221 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where | |
| 222 field | |
| 1172 | 223 p : Ordinal |
| 1142 | 224 op : odef (OS TP) p |
| 225 prod : x ≡ & (ZFP (* p) Q ) | |
| 226 | |
| 227 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where | |
| 228 field | |
| 1172 | 229 q : Ordinal |
| 1142 | 230 oq : odef (OS TQ) q |
| 231 prod : x ≡ & (ZFP P (* q )) | |
| 232 | |
| 233 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x | |
| 1172 | 234 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where |
| 1142 | 235 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) |
| 236 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
| 237 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where | |
| 238 tp03 : odef P a | |
| 239 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa | |
| 1172 | 240 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where |
| 1142 | 241 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) |
| 242 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
| 243 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where | |
| 244 tp03 : odef Q b | |
| 245 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb | |
| 246 | |
| 247 pbase : {P Q : HOD} → Topology P → Topology Q → HOD | |
| 248 pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where | |
| 249 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) | |
| 1150 | 250 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) |
| 1142 | 251 |
| 252 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) | |
| 1152 | 253 ProductTopology {P} {Q} TP TQ = InducedTopology (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } |
| 1142 | 254 |
| 1152 | 255 -- covers ( q ⊆ Union P ) |
| 1101 | 256 |
| 1120 | 257 record _covers_ ( P q : HOD ) : Set n where |
| 431 | 258 field |
| 1120 | 259 cover : {x : Ordinal } → odef q x → Ordinal |
| 1145 | 260 P∋cover : {x : Ordinal } → (lt : odef q x) → odef P (cover lt) |
| 261 isCover : {x : Ordinal } → (lt : odef q x) → odef (* (cover lt)) x | |
| 1120 | 262 |
| 263 open _covers_ | |
| 431 | 264 |
| 265 -- Finite Intersection Property | |
| 266 | |
| 1191 | 267 data Finite-∩ (S : HOD) : Ordinal → Set n where |
| 268 fin-e : Finite-∩ S o∅ | |
| 269 fin-i : {x : Ordinal } → odef S x → Finite-∩ S (& ( * x , * x )) | |
| 270 fin-∩ : {x y : Ordinal } → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (& (* x ∩ * y)) | |
| 271 | |
| 1120 | 272 record FIP {L : HOD} (top : Topology L) : Set n where |
| 431 | 273 field |
| 1150 | 274 limit : {X : Ordinal } → * X ⊆ CS top |
| 1191 | 275 → ( { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) → Ordinal |
| 1150 | 276 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
| 1191 | 277 → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) |
| 1143 | 278 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) |
| 1150 | 279 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
| 1191 | 280 → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) |
| 1150 | 281 → {x : Ordinal } → odef (* X) x |
| 1143 | 282 → odef L (limit CX fip) |
| 283 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) | |
| 431 | 284 |
| 285 -- Compact | |
| 286 | |
| 1119 | 287 data Finite-∪ (S : HOD) : Ordinal → Set n where |
| 1188 | 288 fin-e : Finite-∪ S o∅ |
| 1190 | 289 fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) |
| 1188 | 290 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) |
| 431 | 291 |
| 1120 | 292 record Compact {L : HOD} (top : Topology L) : Set n where |
| 431 | 293 field |
| 1120 | 294 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal |
| 295 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L | |
| 1150 | 296 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) |
| 431 | 297 |
| 298 -- FIP is Compact | |
| 299 | |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
300 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
| 1150 | 301 FIP→Compact {L} top fip with trio< (& L) o∅ |
|
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
302 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
| 1148 | 303 ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where |
| 304 -- L is empty | |
|
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
305 fip02 : {x : Ordinal } → ¬ odef L x |
|
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
306 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) ) |
| 1148 | 307 fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L |
|
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
308 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } |
| 1148 | 309 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅ |
| 1188 | 310 fip00 {X} xo xcp = fin-e |
|
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
311 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where |
| 1121 | 312 -- set of coset of X |
| 313 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal | |
| 1188 | 314 CX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) |
| 1150 | 315 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top |
| 1143 | 316 CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox |
| 317 ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L ＼ * z) | |
| 318 fip07 : z ≡ & (L ＼ * x) | |
| 319 fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where | |
| 320 fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x | |
| 1150 | 321 fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ |
| 1143 | 322 ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ ) |
| 323 fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) | |
| 324 fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , subst (λ k → ¬ odef k w) (sym *iso) fip10 ⟫ where | |
| 325 fip10 : ¬ (odef (L ＼ * z) w) | |
| 326 fip10 ⟪ Lw , nzw ⟫ = nzw zw | |
| 327 fip06 : odef (OS top) (& (L ＼ * x)) | |
| 328 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) | |
| 329 fip05 : * x ⊆ L | |
| 330 fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw ) | |
| 331 -- | |
| 332 -- X covres L means Intersection of (CX X) contains nothing | |
| 1152 | 333 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) |
| 1143 | 334 -- it means there is a finite cover |
| 335 -- | |
| 1191 | 336 finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅ |
| 337 finCoverBase {X} ox oc with ODC.p∨¬p O (Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅) | |
| 1189 | 338 ... | case1 sb = sb |
| 339 ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where | |
| 340 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) | |
| 341 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) | |
| 1148 | 342 -- CX is finite intersection |
| 1191 | 343 fip02 : {x : Ordinal} → Finite-∩ (* (CX ox)) x → o∅ o< x |
| 1187 | 344 fip02 {x} sc with trio< x o∅ |
| 1148 | 345 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
| 346 ... | tri> ¬a ¬b c = c | |
| 1191 | 347 ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (subst₂ (λ j k → Finite-∩ j k ) *iso b sc )) |
| 1150 | 348 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) |
| 1148 | 349 fip26 : odef (* (CX ox)) (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) |
| 1150 | 350 fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) |
| 351 record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } | |
| 1148 | 352 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) |
| 353 fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26 | |
| 354 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) | |
| 355 fip20 {y} Xy yl = proj2 fip21 yl where | |
| 356 fip22 : odef (* (CX ox)) (& ( L ＼ * y )) | |
| 1150 | 357 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } |
| 1148 | 358 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 ) |
| 359 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) | |
| 1191 | 360 finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD |
| 1192 | 361 finCoverSet {X} x fin-e = od∅ |
| 1191 | 362 finCoverSet {X} x (fin-i rx) = ( L ＼ * x ) , ( L ＼ * x ) |
| 363 finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy | |
| 1149 | 364 -- |
| 1121 | 365 -- this defines finite cover |
| 1120 | 366 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
| 1189 | 367 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) |
| 1150 | 368 -- create Finite-∪ from cex |
| 1120 | 369 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
| 1189 | 370 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where |
| 1191 | 371 fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) |
| 1192 | 372 fip60 x fin-e = subst (λ k → Finite-∪ (* X) k) (sym ord-od∅) fin-e |
| 373 fip60 x (fin-i {y} rx) = subst (λ k → Finite-∪ (* X) k) ? (fin-i ?) where | |
| 374 fip63 : odef (Replace (* X) (_＼_ L)) (& (* y , * y)) | |
| 375 fip63 = record { z = ? ; az = ? ; x=ψz = ? } | |
| 1190 | 376 fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) |
| 377 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso | |
| 1189 | 378 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) )) |
| 379 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where | |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
380 fip34 : * z1 ⊆ L |
|
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
381 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1 |
| 1189 | 382 fip33 : z1 ≡ & (L ＼ * x) |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
383 fip33 = begin |
| 1152 | 384 z1 ≡⟨ sym &iso ⟩ |
| 385 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩ | |
| 386 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ | |
| 387 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ | |
| 1189 | 388 & (L ＼ * x ) ∎ where open ≡-Reasoning |
| 1191 | 389 fip60 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx) (fip60 y sy) ) where |
| 1189 | 390 fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy) |
| 391 fip62 = cong (&) ( begin | |
| 392 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ | |
| 393 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning | |
| 1120 | 394 -- is also a cover |
| 395 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | |
| 1190 | 396 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) |
| 397 (fip70 o∅ (finCoverBase xo xcp)) where | |
| 1191 | 398 fip70 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) |
| 399 fip70 x fin-e = ? | |
| 400 fip70 x (fin-i rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } | |
| 401 fip70 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) ? covers | |
| 402 (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where | |
| 1190 | 403 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b)) |
| 404 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) | |
| 405 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ | |
| 1191 | 406 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ |
| 407 fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c | |
| 408 fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) | |
| 409 ; isCover = isCover cov } | |
| 410 fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c | |
| 411 fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) | |
| 412 ; isCover = isCover cov } | |
| 1190 | 413 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) ) |
| 414 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where | |
| 415 fip44 : {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal | |
| 416 fip44 {x} Lab with fip45 {L} {a} {b} Lab | |
| 417 ... | case1 La = cover ca La | |
| 418 ... | case2 Lb = cover cb Lb | |
| 419 fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt) | |
| 420 fip46 {x} Lab with fip45 {L} {a} {b} Lab | |
| 421 ... | case1 La = P∋cover ca La | |
| 422 ... | case2 Lb = P∋cover cb Lb | |
| 423 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x | |
| 424 fip47 {x} Lab with fip45 {L} {a} {b} Lab | |
| 425 ... | case1 La = isCover ca La | |
| 426 ... | case2 Lb = isCover cb Lb | |
|
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
427 |
| 1180 | 428 open _==_ |
| 429 | |
| 1158 | 430 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
| 1180 | 431 Compact→FIP {L} top compact with trio< (& L) o∅ |
| 1175 | 432 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
| 433 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } | |
| 434 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where | |
| 435 -- set of coset of X | |
| 436 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal | |
| 1188 | 437 OX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) |
| 1175 | 438 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top |
| 439 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox | |
| 440 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where | |
| 441 comp01 : odef (* X) (& (* z)) | |
| 442 comp01 = subst (λ k → odef (* X) k) (sym &iso) az | |
| 1178 | 443 |
| 1183 | 444 -- if all finite intersection of X contains something, |
| 1175 | 445 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) |
| 446 -- it means there is a limit | |
| 1191 | 447 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
| 1180 | 448 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) |
| 1186 | 449 has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where |
| 450 fp07 : HOD -- we have an element of X | |
| 451 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
| 452 fp08 : odef (* X) (& fp07) | |
| 453 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
| 1183 | 454 no-cover : ¬ ( (* (OX CX)) covers L ) |
| 1187 | 455 no-cover cov = ⊥-elim ( ? ) where |
| 1180 | 456 fp01 : Ordinal |
| 457 fp01 = Compact.finCover compact (OOX CX) cov | |
| 1191 | 458 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Finite-∩ (* X) (& ( L ＼ * t ) ) |
| 459 fp02 t fin-e = ? | |
| 460 fp02 t (fin-i tx ) = ? where | |
| 1187 | 461 fp03 : odef (* X) (& (L ＼ * t)) |
| 462 fp03 = ? | |
| 1191 | 463 fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Finite-∩ (* X) k ) fp04 ( fin-∩ (fp02 tx x) (fp02 ty y ) ) where |
| 1187 | 464 fp04 : & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) |
| 465 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where | |
| 466 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x | |
| 467 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt | |
| 468 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where | |
| 469 fp06 : ¬ odef (* tx ∪ * ty) x | |
| 470 fp06 (case1 tx) = ¬tx tx | |
| 471 fp06 (case2 ty) = ¬ty ty | |
| 472 fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x | |
| 473 fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt | |
| 474 ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) | |
| 475 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ | |
| 476 | |
| 1186 | 477 record NC : Set n where -- x is not covered |
| 1183 | 478 field |
| 1185 | 479 x : Ordinal |
| 480 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x | |
| 1186 | 481 not-covered : NC |
| 482 not-covered with ODC.p∨¬p O NC | |
| 1184 | 483 ... | case1 nc = nc |
| 1185 | 484 ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → & (L ＼ coverf Lx) ; P∋cover = fp22 ; isCover = fp23 } ) where |
| 485 coverSet : {x : Ordinal} → odef L x → HOD | |
| 1186 | 486 coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X |
| 487 ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) } | |
| 1185 | 488 fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ ) |
| 1187 | 489 fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where |
| 1185 | 490 fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x |
| 491 fp19 {y} Xy with ∨L＼X {L} {* y} {x} Lx | |
| 492 ... | case1 yx = yx | |
| 493 ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where | |
| 494 fp20 : odef (* X) y ∧ odef (L ＼ * y) x | |
| 495 fp20 = ⟪ Xy , lyx ⟫ | |
| 496 coverf : {x : Ordinal} → (Lx : odef L x ) → HOD | |
| 497 coverf Lx = ODC.minimal O (coverSet Lx) (fp17 Lx) | |
| 1186 | 498 fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt)) |
| 499 fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) (sym *iso) record { z = _ ; az = fp25 ; x=ψz = fp24 } where | |
| 500 fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx))) | |
| 501 fp24 = cong (λ k → & ( L ＼ k )) (sym *iso) | |
| 1185 | 502 fp25 : odef (* X) (& (coverf Lx)) |
| 503 fp25 = proj1 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) ) | |
| 1186 | 504 fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x |
| 505 fp23 {x} Lx = subst (λ k → odef k x) (sym *iso) ⟪ Lx , fp26 ⟫ where | |
| 506 fp26 : ¬ odef (coverf Lx) x | |
| 507 fp26 = subst (λ k → ¬ odef k x ) *iso (proj2 (proj2 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) )) ) | |
| 508 fp05 : {y : Ordinal } → (Xy : odef (* X) y ) → odef ( * y) (NC.x not-covered ) | |
| 509 fp05 {y} Xy = NC.yx not-covered Xy | |
| 510 fp06 : NC.x not-covered o≤ & (* X) | |
| 511 fp06 = begin | |
| 512 NC.x not-covered ≡⟨ sym &iso ⟩ | |
| 513 & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ | |
| 514 & fp07 <⟨ c<→o< fp08 ⟩ | |
| 515 & (* X) ∎ where open o≤-Reasoning O | |
| 1191 | 516 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
| 1175 | 517 → Ordinal |
| 1180 | 518 limit {X} CX fip with trio< X o∅ |
| 519 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
| 520 ... | tri≈ ¬a b ¬c = o∅ | |
| 521 ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c)) | |
| 1175 | 522 fip00 : {X : Ordinal} (CX : * X ⊆ CS top) |
| 1191 | 523 (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
| 1175 | 524 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) |
| 1180 | 525 fip00 {X} CX fip {x} Xx with trio< X o∅ |
| 526 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
| 527 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) ) | |
| 528 ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c ) | |
| 529 ... | ⟪ 0<m , intersect ⟫ = intersect Xx | |
| 1175 | 530 |
| 431 | 531 |
|
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
532 open Filter |
| 1102 | 533 |
| 431 | 534 -- Ultra Filter has limit point |
| 535 | |
| 1159 | 536 record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where |
| 537 field | |
| 538 u : Ordinal | |
| 539 ou : odef (OS TP) u | |
| 540 ux : odef (* u) x | |
| 541 v⊆P : * v ⊆ P | |
| 1170 | 542 u⊆v : * u ⊆ * v |
| 1102 | 543 |
| 1169 | 544 -- |
| 545 -- Neighbor on x is a Filter (on Power P) | |
| 546 -- | |
| 1170 | 547 NeighborF : {P : HOD} (TP : Topology P) (x : Ordinal ) → Filter {Power P} {P} (λ x → x) |
| 1169 | 548 NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = f2 } where |
| 1168 | 549 nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v |
| 550 nf00 {v} nei y vy = Neighbor.v⊆P nei vy | |
| 1167 | 551 NF : HOD |
| 1168 | 552 NF = record { od = record { def = λ v → Neighbor TP x v } ; odmax = & (Power P) ; <odmax = λ lt → odef< (nf00 lt) } |
| 1167 | 553 NF⊆PP : NF ⊆ Power P |
| 1168 | 554 NF⊆PP = nf00 |
| 555 f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q | |
| 1170 | 556 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 |
| 1168 | 557 f11 : * (Neighbor.u Np) ⊆ * (& q) |
| 1170 | 558 f11 {x} ux = subst (λ k → odef k x ) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso (Neighbor.u⊆v Np ux)) ) |
| 1168 | 559 f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q) |
| 1170 | 560 f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where |
| 1168 | 561 upq : Ordinal |
| 562 upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) ) | |
| 563 ou : odef (OS TP) upq | |
| 564 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)) | |
| 565 ux : odef (* upq) x | |
| 1170 | 566 ux = subst ( λ k → odef k x ) (sym *iso) ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ |
| 1168 | 567 f20 : * upq ⊆ * (& (p ∩ q)) |
| 568 f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq | |
| 1170 | 569 → ⟪ subst (λ k → odef k x) *iso (Neighbor.u⊆v Np (proj1 pq)) , subst (λ k → odef k x) *iso (Neighbor.u⊆v Nq (proj2 pq)) ⟫ ) |
| 1153 | 570 |
| 1165 | 571 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q) |
| 572 CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) *iso pqx | |
| 573 ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px ) | |
| 574 | |
| 1170 | 575 NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p ) |
| 576 NEG P {p} Pp x vx with subst (λ k → odef k x) *iso vx | |
| 577 ... | ⟪ Px , npx ⟫ = Px | |
| 1142 | 578 |