Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Topology.agda @ 1117:53ca3c609f0e
generated topology from subbase done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Jan 2023 20:07:04 +0900 |
parents | 6386019deef1 |
children | 441ad880a45d |
comparison
equal
deleted
inserted
replaced
1116:6386019deef1 | 1117:53ca3c609f0e |
---|---|
69 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } | 69 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } |
70 | 70 |
71 record Base (L P : HOD) (u x : Ordinal) : Set n where | 71 record Base (L P : HOD) (u x : Ordinal) : Set n where |
72 field | 72 field |
73 b : Ordinal | 73 b : Ordinal |
74 u⊂L : * u ⊂ L | 74 u⊂L : * u ⊆ L |
75 sb : Subbase P b | 75 sb : Subbase P b |
76 b⊆u : * b ⊆ * u | 76 b⊆u : * b ⊆ * u |
77 bx : odef (* b) x | 77 bx : odef (* b) x |
78 | 78 |
79 SO : (L P : HOD) → HOD | 79 SO : (L P : HOD) → HOD |
91 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L | 91 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
92 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 | 92 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
93 ; o∪ = tp02 ; o∩ = tp01 } where | 93 ; o∪ = tp02 ; o∩ = tp01 } where |
94 tp00 : SO L P ⊆ Power L | 94 tp00 : SO L P ⊆ Power L |
95 tp00 {u} ou x ux with ou ux | 95 tp00 {u} ou x ux with ou ux |
96 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = proj2 u⊂L (b⊆u bx) | 96 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) |
97 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) | 97 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
98 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊂ L) (sym *iso) ul | 98 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul |
99 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where | 99 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
100 px : odef (* (& p)) x | 100 px : odef (* (& p)) x |
101 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | 101 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) |
102 qx : odef (* (& q)) x | 102 qx : odef (* (& q)) x |
103 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | 103 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) |
113 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) | 113 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) |
114 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q | 114 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q |
115 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) | 115 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) |
116 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | 116 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x |
117 tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ | 117 tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ |
118 ul : (p ∩ q) ⊂ L | 118 ul : (p ∩ q) ⊆ L |
119 ul = subst (λ k → k ⊂ L ) *iso ⟪ tp02 , (λ {z} pq → proj2 (Base.u⊂L (op px)) (pz pq) ) ⟫ where | 119 ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq → (Base.u⊂L (op px)) (pz pq) ) where |
120 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z | 120 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
121 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | 121 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) |
122 tp02 : & (* (& (p ∩ q))) o< & L | |
123 tp02 = subst ( λ k → k o< & L) (sym &iso) ? | |
124 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q | 122 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q |
125 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux | 123 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux |
126 ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | 124 ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx |
127 ... | 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 | 125 ... | 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 |
128 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where | 126 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where |
129 tp05 : Union q ⊆ L | 127 tp05 : Union q ⊆ L |
130 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | 128 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx |
131 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | 129 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } |
132 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) | 130 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) |
133 tp04 : Union q ⊂ L | 131 tp04 : Union q ⊆ L |
134 tp04 = ⟪ ? , tp05 ⟫ | 132 tp04 = tp05 |
135 tp06 : * b ⊆ Union q | 133 tp06 : * b ⊆ Union q |
136 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } | 134 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } |
137 | 135 |
138 -- covers | 136 -- covers |
139 | 137 |