Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Tychonoff.agda @ 1202:d6781ad8149e
...
author | kono |
---|---|
date | Thu, 02 Mar 2023 12:42:22 +0800 |
parents | 03684784bc5f |
children | 2f09ce1dd2a1 |
rev | line source |
---|---|
1175 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
431 | 2 open import Level |
3 open import Ordinals | |
1170 | 4 module Tychonoff {n : Level } (O : Ordinals {n}) where |
431 | 5 |
6 open import zf | |
7 open import logic | |
8 open _∧_ | |
9 open _∨_ | |
10 open Bool | |
11 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
12 import OD |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
13 open import Relation.Nullary |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
14 open import Data.Empty |
431 | 15 open import Relation.Binary.Core |
1143 | 16 open import Relation.Binary.Definitions |
431 | 17 open import Relation.Binary.PropositionalEquality |
1124 | 18 import BAlgebra |
19 open BAlgebra O | |
431 | 20 open inOrdinal O |
21 open OD O | |
22 open OD.OD | |
23 open ODAxiom odAxiom | |
24 import OrdUtil | |
25 import ODUtil | |
26 open Ordinals.Ordinals O | |
27 open Ordinals.IsOrdinals isOrdinal | |
28 open Ordinals.IsNext isNext | |
29 open OrdUtil O | |
30 open ODUtil O | |
31 | |
32 import ODC | |
33 open ODC O | |
34 | |
1102 | 35 open import filter O |
1101 | 36 open import OPair O |
1170 | 37 open import Topology O |
1201 | 38 -- open import maximum-filter O |
431 | 39 |
1170 | 40 open Filter |
41 open Topology | |
1169 | 42 |
431 | 43 -- FIP is UFL |
44 | |
1159 | 45 -- filter Base |
46 record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where | |
1153 | 47 field |
1161 | 48 b x : Ordinal |
1155 | 49 b⊆X : * b ⊆ * X |
1161 | 50 sb : Subbase (* b) x |
1158 | 51 u⊆P : * u ⊆ P |
1154 | 52 x⊆u : * x ⊆ * u |
1155 | 53 |
1170 | 54 record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) ) |
55 (ultra : ultra-filter F ) : Set (suc (suc n)) where | |
56 field | |
57 limit : Ordinal | |
58 P∋limit : odef P limit | |
59 is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F | |
1165 | 60 |
1161 | 61 UFLP→FIP : {P : HOD} (TP : Topology P) → |
1169 | 62 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP |
1163 | 63 UFLP→FIP {P} TP uflp with trio< (& P) o∅ |
64 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
1201 | 65 ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where |
1163 | 66 -- P is empty |
67 fip02 : {x : Ordinal } → ¬ odef P x | |
1201 | 68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) ) |
69 fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} → | |
70 odef (* X) x → odef (* x) o∅ | |
71 -- empty P case | |
72 -- if 0 < X then 0 < x ∧ P ∋ xfrom fip | |
73 -- if 0 ≡ X then ¬ odef X x | |
74 fip03 {X} CX fip {x} xx with trio< o∅ X | |
75 ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) | |
76 ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where | |
77 0<x : o∅ o< x | |
78 0<x = fip (gi xx ) | |
79 e : HOD -- we have an element of x | |
80 e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
81 xe : odef (* x) (& e) | |
82 xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin | |
84 * X ≡⟨ cong (*) (sym 0=X) ⟩ | |
85 * o∅ ≡⟨ o∅≡od∅ ⟩ | |
86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning | |
87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → UFLP.limit (uflp (F CSX fip) (ultraf CSX fip)) ; is-limit = ? } where | |
1143 | 89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
1187 | 90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x |
1154 | 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
1161 | 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
1159 | 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
1158 | 94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
1159 | 95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
1202 | 96 -- filter base is not empty |
1201 | 97 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD |
98 nc {X} CSX fip with trio< o∅ X | |
99 ... | tri< 0<X ¬b ¬c = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where | |
100 e : HOD -- we have an element of X | |
101 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
102 Xe : odef (* X) (& e) | |
103 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
104 ... | tri≈ ¬a b ¬c = od∅ | |
105 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
106 N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc CSX fip) ) | |
107 N∋nc {X} CSX fip with trio< o∅ X | |
108 ... | tri< 0<X ¬b ¬c = record { b = ? ; x = ? ; b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where | |
109 e : HOD -- we have an element of X | |
110 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
111 Xe : odef (* X) (& e) | |
112 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
113 nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) | |
114 ... | tri≈ ¬a b ¬c = ? -- od∅ | |
115 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
1165 | 116 0<PP : o∅ o< & (Power P) |
1201 | 117 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where |
118 nn00 : odef (Power P) o∅ | |
119 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt | |
120 ... | x<0 = ⊥-elim ( ¬x<0 x<0) | |
1174 | 121 -- |
122 -- FIP defines a filter | |
123 -- | |
1158 | 124 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) |
125 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where | |
126 f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q | |
1161 | 127 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = |
128 record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → | |
1158 | 129 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where |
130 f10 : q ⊆ P | |
131 f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) | |
132 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) | |
133 f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where | |
134 p∩q⊆p : * (& (p ∩ q)) ⊆ P | |
135 p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) | |
1159 | 136 Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) |
137 xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) | |
1155 | 138 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) |
1159 | 139 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) |
1155 | 140 f20 : * (& Np+Nq) ⊆ * X |
141 f20 {x} npq with subst (λ k → odef k x) *iso npq | |
1159 | 142 ... | case1 np = FBase.b⊆X Np np |
143 ... | case2 nq = FBase.b⊆X Nq nq | |
1155 | 144 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q)) |
1161 | 145 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq |
1159 | 146 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) |
1174 | 147 -- |
148 -- it contains no empty sets | |
149 -- | |
1155 | 150 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅) |
151 proper = ? | |
1174 | 152 -- |
153 -- then we have maximum ultra filter | |
154 -- | |
1158 | 155 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) |
1201 | 156 maxf {X} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) |
1170 | 157 mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) |
158 mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp) | |
159 ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp) | |
1201 | 160 ultraf {X} CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) |
1174 | 161 -- |
162 -- so i has a limit as a limit of UIP | |
163 -- | |
1170 | 164 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
165 limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) | |
166 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) | |
167 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp ) | |
168 uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx | |
1174 | 169 -- |
1201 | 170 -- the limit is an limit of entire elements of X |
1174 | 171 -- |
1170 | 172 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) |
173 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp)) | |
174 ... | yes y = subst (λ k → odef (* x) k) &iso y | |
175 ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 ) where | |
176 uf03 : OS TP ∋ ( P \ (* x)) | |
177 uf03 = ? | |
178 uf05 : odef ( P \ (* x)) (limit CSX fp) | |
179 uf05 = ⟪ ? , subst (λ k → ¬ odef (* x) k) ? nxl ⟫ | |
180 uf04 : Neighbor TP (limit CSX fp) (& ( P \ (* (limit CSX fp)))) | |
181 uf04 = record { u = & ( P \ (* x)) ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ? } | |
182 uf07 : odef (filter (mf CSX fp)) x | |
183 uf07 = ? | |
184 uf06 : odef (filter (mf CSX fp)) (& ( P \ (* x)) ) | |
185 uf06 = ? | |
186 uf08 : (filter (mf CSX fp)) ∋ od∅ | |
187 uf08 = ? | |
1169 | 188 |
1142 | 189 |
1158 | 190 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
1169 | 191 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF |
1201 | 192 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where |
1174 | 193 -- |
194 -- take closure of given filter elements | |
195 -- | |
1160 | 196 CF : HOD |
1188 | 197 CF = Replace (filter F) (λ x → Cl TP x ) |
1160 | 198 CF⊆CS : CF ⊆ CS TP |
1162 | 199 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) |
1174 | 200 -- |
201 -- it is set of closed set and has FIP ( F is proper ) | |
202 -- | |
1187 | 203 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x |
1162 | 204 ufl01 = ? |
1174 | 205 -- |
206 -- so we have a limit | |
207 -- | |
1170 | 208 limit : Ordinal |
1201 | 209 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 |
1170 | 210 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit |
1201 | 211 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 |
1174 | 212 -- |
213 -- Neigbor of limit ⊆ Filter | |
214 -- | |
1171 | 215 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF which is a closure |
1170 | 216 ufl03 {f} {v} ff nei fv=0 = ? |
217 pp : {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x) | |
218 pp {v} {x} nei vx z pz = ? | |
219 ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F | |
220 ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx)) | |
221 ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv | |
1171 | 222 ... | case2 nfv = ? -- will contradicts ufl03 |
1163 | 223 |
1124 | 224 -- product topology of compact topology is compact |
431 | 225 |
1142 | 226 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) |
1158 | 227 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where |
1169 | 228 uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F) |
229 → UFLP TP F UF | |
230 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF | |
231 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) | |
232 → UFLP TQ F UF | |
233 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF | |
1201 | 234 -- Product of UFL has a limit point |
1169 | 235 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) |
236 → UFLP (ProductTopology TP TQ) F UF | |
237 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where | |
238 FP : Filter {Power P} {P} (λ x → x) | |
1164 | 239 FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where |
1169 | 240 ty00 : Proj1 (filter F) (Power P) (Power Q) ⊆ Power P |
241 ty00 {x} ⟪ PPx , ppf ⟫ = PPx | |
1161 | 242 UFP : ultra-filter FP |
1159 | 243 UFP = record { proper = ? ; ultra = ? } |
1169 | 244 uflp : UFLP TP FP UFP |
245 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP | |
1154 | 246 |
1169 | 247 FQ : Filter {Power Q} {Q} (λ x → x) |
1166 | 248 FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where |
1169 | 249 ty00 : Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q |
250 ty00 {x} ⟪ QPx , ppf ⟫ = QPx | |
1166 | 251 UFQ : ultra-filter FQ |
252 UFQ = record { proper = ? ; ultra = ? } | |
1169 | 253 uflq : UFLP TQ FQ UFQ |
254 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ | |
1154 | 255 |
1166 | 256 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
257 Pf = ? | |
1171 | 258 pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F |
1170 | 259 pq⊆F = ? |
260 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F | |
1173 | 261 isL {v} npq {x} fx = ? where |
1172 | 262 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
263 bpq = Neighbor.ou npq (Neighbor.ux npq) | |
264 pqb : Subbase (pbase TP TQ) (Base.b bpq ) | |
265 pqb = Base.sb bpq | |
1173 | 266 pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq ) |
267 pqb⊆opq = Base.b⊆u bpq | |
268 base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → * b ⊆ filter F | |
269 base⊆F (gi (case1 px)) b⊆u {z} bz = fz where | |
270 -- F contains no od∅, because it projection contains no od∅ | |
271 -- x is an element of BaseP, which is a subset of Neighbor npq | |
272 -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp) | |
273 -- BaseP ∩ F is not empty | |
274 -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , | |
275 il1 : odef (Power P) z ∧ ZProj1 (filter F) z | |
276 il1 = UFLP.is-limit uflp ? bz | |
277 nei1 : HOD | |
278 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q) | |
279 plimit : Ordinal | |
1174 | 280 plimit = UFLP.limit uflp |
1173 | 281 nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b |
282 nproper = ? | |
283 b∋z : odef nei1 z | |
284 b∋z = ? | |
285 bp : BaseP {P} TP Q z | |
1187 | 286 bp = record { p = ? ; op = ? ; prod = ? } |
1173 | 287 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F |
288 neip = ? | |
289 il2 : * z ⊆ ZFP (Power P) (Power Q) | |
290 il2 = ? | |
291 il3 : filter F ∋ ? | |
292 il3 = ? | |
293 fz : odef (filter F) z | |
294 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?) | |
295 base⊆F (gi (case2 qx)) b⊆u {z} bz = ? | |
296 base⊆F (g∩ b1 b2) b⊆u {z} bz = ? | |
1154 | 297 |
1170 | 298 |
299 | |
300 | |
301 | |
302 |