Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Tychonoff.agda @ 1279:7e7d8d825632
P x Q ⇆ Q x P done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Apr 2023 09:16:52 +0900 |
| parents | b15dd4438d50 |
| children | f4dac8be0a01 |
| 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 |
| 1218 | 36 open import ZProduct O |
| 1170 | 37 open import Topology O |
| 1279 | 38 open import maximum-filter O |
| 431 | 39 |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
40 open Filter |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
41 open Topology |
| 1169 | 42 |
| 1237 | 43 -- |
| 44 -- Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) | |
| 45 -- → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) | |
| 46 -- | |
| 47 -- ULFP : Compact <=> Every ultra filter F have a limit i.e. open sets which contains the limit (Neighbor limit) is in F | |
| 48 -- | |
| 49 -- Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where | |
| 50 -- | |
| 51 -- FP FQ : create projections of a filter F, so it is ULFP | |
| 52 -- | |
| 53 -- Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) | |
| 54 -- | |
| 55 -- the product of each limits must be a limit of ultra filter F | |
| 56 -- | |
| 57 -- its neighbor is in F, because we can decompose Neighbors nei into subbase of Product Topology which is a open set of P ∋ p or Q ∋ q | |
| 58 -- so (P x q) ∋ limit ∨ (q x P) ∋ limit. P x q ⊆ nei , so nei ∋ limit | |
| 59 -- | |
| 60 -- uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) | |
| 61 -- → UFLP (ProductTopology TP TQ) F UF | |
| 62 -- | |
| 63 -- QED. | |
| 64 | |
| 431 | 65 -- FIP is UFL |
| 66 | |
| 1159 | 67 -- filter Base |
| 1205 | 68 record FBase (P : HOD ) (X : Ordinal ) (u : Ordinal) : Set n where |
| 1153 | 69 field |
| 1161 | 70 b x : Ordinal |
| 1155 | 71 b⊆X : * b ⊆ * X |
| 1161 | 72 sb : Subbase (* b) x |
| 1158 | 73 u⊆P : * u ⊆ P |
| 1154 | 74 x⊆u : * x ⊆ * u |
| 1155 | 75 |
| 1170 | 76 record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) ) |
| 77 (ultra : ultra-filter F ) : Set (suc (suc n)) where | |
| 78 field | |
| 79 limit : Ordinal | |
| 80 P∋limit : odef P limit | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
81 is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v) |
| 1165 | 82 |
| 1279 | 83 -- |
| 84 -- If Any ultra filter has a limit that is all neighbor of the limit is in the filter, | |
| 85 -- it has finite intersection property. | |
| 86 -- | |
| 87 -- Finite intersection defines a filter, so we have a ultra filter becaause Zorn lemma maximizing it. | |
| 88 -- If the limit of filter is not contained by a closed set p in FIP, it is in P \ p. It is open and | |
| 89 -- contains the limit, so it is in the ultra filter. This means p and P \ p is in the filter, which | |
| 90 -- contradicts proper of the ultra filter. | |
| 91 -- | |
| 1161 | 92 UFLP→FIP : {P : HOD} (TP : Topology P) → |
| 1169 | 93 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP |
| 1163 | 94 UFLP→FIP {P} TP uflp with trio< (& P) o∅ |
| 95 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
| 1201 | 96 ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where |
| 1237 | 97 -- P is empty ( this case cannot happen because ulfp → 0 < P ) |
| 1163 | 98 fip02 : {x : Ordinal } → ¬ odef P x |
| 1201 | 99 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) ) |
| 100 fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} → | |
| 101 odef (* X) x → odef (* x) o∅ | |
| 102 -- empty P case | |
| 103 -- if 0 < X then 0 < x ∧ P ∋ xfrom fip | |
| 104 -- if 0 ≡ X then ¬ odef X x | |
| 105 fip03 {X} CX fip {x} xx with trio< o∅ X | |
| 106 ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) | |
| 107 ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where | |
| 108 0<x : o∅ o< x | |
| 109 0<x = fip (gi xx ) | |
| 110 e : HOD -- we have an element of x | |
| 111 e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
| 112 xe : odef (* x) (& e) | |
| 113 xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
| 114 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin | |
| 115 * X ≡⟨ cong (*) (sym 0=X) ⟩ | |
| 116 * o∅ ≡⟨ o∅≡od∅ ⟩ | |
| 117 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning | |
| 118 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
| 1204 | 119 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = uf01 } where |
| 1143 | 120 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
| 1187 | 121 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x |
| 1154 | 122 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
| 1161 | 123 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
| 1159 | 124 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
| 1158 | 125 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
| 1159 | 126 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
| 1237 | 127 -- filter base is not empty, it is necessary to maximize fip filter |
| 1204 | 128 nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD |
| 1205 | 129 nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
130 N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) |
| 1204 | 131 → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) ) |
| 1205 | 132 N∋nc {X} 0<X CSX fip = record { b = X ; x = & e ; b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where |
| 1201 | 133 e : HOD -- we have an element of X |
| 134 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
| 135 Xe : odef (* X) (& e) | |
| 136 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
137 nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) |
| 1205 | 138 nn02 : * (& (nc 0<X CSX fip)) ⊆ P |
| 139 nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) ) | |
| 140 | |
| 1237 | 141 0<PP : o∅ o< & (Power P) -- Power P contaisn od∅, so it is not empty |
| 1201 | 142 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where |
| 143 nn00 : odef (Power P) o∅ | |
| 144 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt | |
| 145 ... | x<0 = ⊥-elim ( ¬x<0 x<0) | |
| 1174 | 146 -- |
| 147 -- FIP defines a filter | |
| 148 -- | |
| 1158 | 149 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) |
| 150 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where | |
| 151 f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q | |
| 1161 | 152 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = |
| 153 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 | 154 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where |
| 155 f10 : q ⊆ P | |
| 156 f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) | |
| 157 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) | |
| 158 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 | |
| 159 p∩q⊆p : * (& (p ∩ q)) ⊆ P | |
| 160 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 | 161 Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) |
| 162 xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) | |
| 1155 | 163 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) |
| 1159 | 164 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) |
| 1155 | 165 f20 : * (& Np+Nq) ⊆ * X |
| 166 f20 {x} npq with subst (λ k → odef k x) *iso npq | |
| 1159 | 167 ... | case1 np = FBase.b⊆X Np np |
| 168 ... | case2 nq = FBase.b⊆X Nq nq | |
| 1155 | 169 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q)) |
| 1161 | 170 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq |
| 1159 | 171 → ⟪ 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 | 172 -- |
| 1207 | 173 -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x ) |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
174 -- |
| 1207 | 175 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅) |
| 176 proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where | |
| 177 x≤0 : x o< osuc o∅ | |
| 178 x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u)) | |
| 179 fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x | |
| 180 fp00 b y b<X (gi by ) = gi ( b<X by ) | |
| 181 fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz) | |
| 1174 | 182 -- |
| 1237 | 183 -- then we have maximum ultra filter ( Zorn lemma ) |
| 1239 | 184 -- to debug this file, commet out the maximum filter and open import |
| 1237 | 185 -- otherwise the check requires a minute |
| 1174 | 186 -- |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
187 maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) |
| 1279 | 188 maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
189 mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
190 mf {X} 0<X CSX fp = MaximumFilter.mf (maxf 0<X CSX fp) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
191 ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp) |
| 1279 | 192 ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) |
| 1174 | 193 -- |
| 1279 | 194 -- so it has a limit as a limit of FIP |
| 1174 | 195 -- |
| 1170 | 196 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
| 1203 | 197 limit {X} CSX fp with trio< o∅ X |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
198 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
199 ... | tri≈ ¬a 0=X ¬c = o∅ |
| 1203 | 200 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
| 1174 | 201 -- |
| 1201 | 202 -- the limit is an limit of entire elements of X |
| 1174 | 203 -- |
| 1170 | 204 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) |
| 1204 | 205 uf01 {X} CSX fp {x} xx with trio< o∅ X |
| 1206 | 206 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
| 1205 | 207 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx ))) |
| 1237 | 208 -- 0<X limit is in * x or P ＼ * x |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
209 ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))} |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
210 (UFLP.P∋limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))) |
| 1206 | 211 ... | case1 lt = lt -- odef (* x) y |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
212 ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where |
| 1237 | 213 -- |
| 214 -- if (* x) do not conatins a limit, P ＼ * x contains it, (P ＼ * x) is open so it is the maxf ( UFLP.is-limit ) | |
| 215 -- UFLP contains (* x) and P ＼ * x, it contains od∅, contradicts the proper | |
| 216 -- | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
217 y = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) |
| 1207 | 218 x⊆P : * x ⊆ P |
| 219 x⊆P = cs⊆L TP (CSX (subst (λ k → odef (* X) k) (sym &iso) xx)) | |
| 1206 | 220 uf10 : odef (P ＼ * x ) y |
| 221 uf10 = nlxy | |
| 222 uf03 : Neighbor TP y (& (P ＼ * x )) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
223 uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
224 ; ux = subst (λ k → odef k y) (sym *iso) uf10 |
| 1206 | 225 ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz ) |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
226 ; u⊆v = λ x → x } |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
227 uf07 : * (& (* x , * x)) ⊆ * X |
| 1207 | 228 uf07 {y} lt with subst (λ k → odef k y) *iso lt |
| 229 ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx | |
| 230 ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
231 uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
232 uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 |
| 1207 | 233 ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) ) ; u⊆P = x⊆P ; x⊆u = λ x → x } |
| 1213 | 234 uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x )))) |
| 235 uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03 | |
| 236 -- uf06 (same as uf061) have yellow if zorn lemma is not imported | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
237 uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x )) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
238 uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso (UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03 ) |
| 1206 | 239 uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅ |
| 1207 | 240 uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) } ) ) where |
| 241 uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y | |
| 242 uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy ) | |
| 1206 | 243 uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x ))) |
| 1207 | 244 uf12 z pz with subst (λ k → odef k z) *iso pz |
| 245 ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
246 uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅ |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
247 uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅)) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
248 ( filter2 (MaximumFilter.mf (maxf 0<X CSX fp)) (subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) (sym &iso) uf05) uf06 uf12 ) |
| 1142 | 249 |
| 1208 | 250 x⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → x ⊆ Cl TP x |
| 251 x⊆Clx {P} TP {x} x<p {y} xy = ⟪ x<p xy , (λ c csc x<c → x<c xy ) ⟫ | |
| 252 P⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → Cl TP x ⊆ P | |
| 253 P⊆Clx {P} TP {x} x<p {y} xy = proj1 xy | |
| 254 | |
| 1279 | 255 -- |
| 256 -- Finite intersection property implies that any ultra filter have a limit, that is, neighbors of the limit is in the filter. | |
| 257 -- | |
| 258 -- An ultra filter F is given. Take a closure of a filter. It is closed and it has finite intersection property, because F is porper. | |
| 259 -- So it has a limit as a FIP. If a neighbor p which contains the limit, p or P \ p is in the ultra filter. | |
| 260 -- If it is in P \ p, it cannot contains the limit, contradiction. | |
| 261 -- | |
| 1158 | 262 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
| 1169 | 263 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
264 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
| 1209 | 265 ; P∋limit = ufl10 ; is-limit = ufl00 } where |
| 266 F∋P : odef (filter F) (& P) | |
| 267 F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) | |
| 268 ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) | |
| 269 ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where | |
| 270 fl20 : (P ＼ Ord o∅) =h= P | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
271 fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } |
| 1209 | 272 0<P : o∅ o< & P |
| 273 0<P with trio< o∅ (& P) | |
| 274 ... | tri< a ¬b ¬c = a | |
| 275 ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋P) ) | |
| 276 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
| 1174 | 277 -- |
| 278 -- take closure of given filter elements | |
| 279 -- | |
| 1160 | 280 CF : HOD |
| 1188 | 281 CF = Replace (filter F) (λ x → Cl TP x ) |
| 1160 | 282 CF⊆CS : CF ⊆ CS TP |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
283 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 | 284 -- |
| 285 -- it is set of closed set and has FIP ( F is proper ) | |
| 286 -- | |
| 1208 | 287 ufl08 : {z : Ordinal} → odef (Power P) (& (Cl TP (* z))) |
| 288 ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw | |
| 289 ... | t = proj1 t | |
| 290 fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x | |
| 291 fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz ) | |
| 292 F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x | |
| 293 F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where | |
| 294 ufl09 : * z ⊆ P | |
| 295 ufl09 {y} zy = f⊆L F az _ zy | |
| 296 ufl07 : odef (filter F) x | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
297 ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 ) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
298 (subst (λ k → odef (filter F) k) (sym &iso) az) |
| 1208 | 299 (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) )) |
| 300 F∋sb (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx)) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
301 (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
302 (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) ))) |
| 1187 | 303 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x |
| 1208 | 304 ufl01 {x} sb = ufl04 where |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
305 ufl04 : o∅ o< x |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
306 ufl04 with trio< o∅ x |
| 1208 | 307 ... | tri< a ¬b ¬c = a |
| 308 ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) ( | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
309 begin |
| 1208 | 310 x ≡⟨ sym b ⟩ |
| 311 o∅ ≡⟨ sym ord-od∅ ⟩ | |
| 312 & od∅ ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) )) where open ≡-Reasoning | |
| 313 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
| 1209 | 314 ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01) |
| 315 ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11 where | |
| 316 ufl11 : odef (* (& CF)) (& P) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
317 ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP))) } |
| 1174 | 318 -- |
| 319 -- so we have a limit | |
| 320 -- | |
| 1170 | 321 limit : Ordinal |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
322 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
| 1170 | 323 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
324 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
| 1174 | 325 -- |
| 326 -- Neigbor of limit ⊆ Filter | |
| 327 -- | |
| 1210 | 328 -- if odef (* X) x, Cl TP x contains limit (ufl02) |
| 329 -- in (nei : Neighbor TP limit v) , there is an open Set u which contains the limit | |
| 330 -- F contains u or P ＼ u because F is ultra | |
| 331 -- if F ∋ u, then F ∋ v from u ⊆ v which is a propetery of Neighbor | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
332 -- if F ∋ P ＼ u, it is a closed set (Cl (P ＼ u) ≡ P ＼ u) and it does not contains the limit |
| 1210 | 333 -- this contradicts ufl02 |
| 334 pp : {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei)) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
335 pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
336 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
337 ufl00 : {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
338 ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei )) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
339 ... | case1 fu = subst (λ k → odef (filter F) k) &iso |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
340 ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px) fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
341 u = * (Neighbor.u nei) |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
342 px : Power P ∋ * v |
|
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
343 px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz ) |
| 1210 | 344 ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where |
| 345 u = * (Neighbor.u nei) | |
| 346 P\u : HOD | |
| 347 P\u = P ＼ u | |
| 348 P\u∋limit : odef P\u limit | |
| 349 P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where | |
| 350 ufl04 : & P\u ≡ & (Cl TP (* (& P\u))) | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
351 ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) |
| 1210 | 352 (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))))) |
| 353 ufl03 : odef CF (& P\u ) | |
| 354 ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 } | |
| 355 ¬P\u∋limit : ¬ odef P\u limit | |
| 356 ¬P\u∋limit ⟪ Pl , nul ⟫ = nul ( Neighbor.ux nei ) | |
| 1163 | 357 |
| 1124 | 358 -- product topology of compact topology is compact |
| 431 | 359 |
| 1218 | 360 import Axiom.Extensionality.Propositional |
| 361 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m | |
| 362 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 363 | |
| 1279 | 364 -- FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) |
| 365 -- → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) | |
| 366 -- FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } | |
| 367 -- | |
| 368 -- projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) | |
| 369 -- → Filter {Power P} {P} (λ x → x) | |
| 370 -- projection-of-filter = ? | |
| 371 -- | |
| 372 -- projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) | |
| 373 -- → ultra-filter (projection-of-filter F) | |
| 374 -- projection-of-ultra-filter = ? | |
| 1274 | 375 |
| 1279 | 376 -- |
| 377 -- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter | |
| 378 -- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q, | |
| 379 -- which is either inverse projection x of P or Q. The x in in projection of F, because of UFLP. So it is in F, because of the | |
| 380 -- property of the filter. | |
| 381 -- | |
| 1142 | 382 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) |
| 1158 | 383 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where |
| 1169 | 384 uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F) |
| 385 → UFLP TP F UF | |
| 386 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF | |
| 387 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) | |
| 388 → UFLP TQ F UF | |
| 389 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF | |
| 1201 | 390 -- Product of UFL has a limit point |
| 1169 | 391 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) |
| 392 → UFLP (ProductTopology TP TQ) F UF | |
| 393 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where | |
| 1213 | 394 F∋PQ : odef (filter F) (& (ZFP P Q)) |
| 395 F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) | |
| 396 ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) | |
| 397 ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where | |
| 398 fl20 : (ZFP P Q ＼ Ord o∅) =h= ZFP P Q | |
| 399 fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } | |
| 1218 | 400 0<PQ : o∅ o< & (ZFP P Q) |
| 401 0<PQ with trio< o∅ (& (ZFP P Q)) | |
| 1213 | 402 ... | tri< a ¬b ¬c = a |
| 403 ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) ) | |
| 404 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
| 1218 | 405 apq : HOD |
| 406 apq = ODC.minimal O (ZFP P Q) (0<P→ne 0<PQ) | |
| 407 is-apq : ZFP P Q ∋ apq | |
| 408 is-apq = ODC.x∋minimal O (ZFP P Q) (0<P→ne 0<PQ) | |
| 409 ap : odef P ( zπ1 is-apq ) | |
| 410 ap = zp1 is-apq | |
| 411 aq : odef Q ( zπ2 is-apq ) | |
| 412 aq = zp2 is-apq | |
| 1223 | 413 F⊆pxq : {x : HOD } → filter F ∋ x → x ⊆ ZFP P Q |
| 414 F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy) | |
| 415 | |
| 1229 | 416 --- |
| 417 --- FP is a P-projection of F, which is a ultra filter | |
| 418 --- | |
| 419 isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q | |
| 1213 | 420 isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q |
| 1229 | 421 fx→px : {x : HOD } → filter F ∋ x → HOD |
| 1216 | 422 fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) |
| 1217 | 423 fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋ ZFP p Q ) → fx→px fp ≡ p |
| 424 fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where | |
| 425 ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) | |
| 1229 | 426 ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz )) |
| 1217 | 427 ty32 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a |
| 428 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where | |
| 429 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a | |
| 430 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 431 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
| 1216 | 432 ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x |
| 1217 | 433 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef p k) a=x pz where |
| 1229 | 434 ty24 : * x ≡ * a |
| 1216 | 435 ty24 = begin |
| 1217 | 436 * x ≡⟨ cong (*) x=ψz ⟩ |
| 437 _ ≡⟨ *iso ⟩ | |
| 438 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 pz qz) ⟩ | |
| 439 * a ∎ where open ≡-Reasoning | |
| 1229 | 440 a=x : a ≡ x |
| 1217 | 441 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) |
| 1229 | 442 ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x |
| 1217 | 443 ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where |
| 444 ty12 : * x ≡ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) | |
| 445 ty12 = begin | |
| 446 * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩ | |
| 447 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning | |
| 1229 | 448 |
| 449 -- Projection of F | |
| 1213 | 450 FPSet : HOD |
| 451 FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))) | |
| 1229 | 452 |
| 453 -- Projection ⁻¹ F (which is in F) is in FPSet | |
| 1215 | 454 FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋ ZFP q Q → FPSet ∋ q |
| 1217 | 455 FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where |
| 1218 | 456 -- brain damaged one |
| 1229 | 457 ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } → |
| 1218 | 458 * (zπ1 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ1 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) |
| 459 ty11 {y} {xy} = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where | |
| 460 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy | |
| 1229 | 461 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) |
| 1217 | 462 ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q |
| 463 ty10 = begin | |
| 1229 | 464 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) |
| 465 ≡⟨ | |
| 1218 | 466 cong (λ k → Replace' (* (& (ZFP q Q))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) |
| 467 ⟩ | |
| 1229 | 468 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) |
| 1218 | 469 ≡⟨ Replace'-iso _ ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ⟩ |
| 1229 | 470 Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ |
| 1218 | 471 fx→px fq ≡⟨ fx→px1 aq fq ⟩ |
| 1217 | 472 q ∎ where open ≡-Reasoning |
| 1213 | 473 FPSet⊆PP : FPSet ⊆ Power P |
| 474 FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw | |
| 1229 | 475 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } |
| 476 = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) | |
| 1213 | 477 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) |
| 1223 | 478 X=F1 : (x : Ordinal) (p : HOD) (fx : odef (filter F) x) → Set n |
| 479 X=F1 x p fx = & p ≡ & (Replace' (* x) (λ y xy → | |
| 1222 | 480 * (zπ1 (f⊆L F |
| 481 (subst (odef (filter F)) (sym &iso) fx) | |
| 482 (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy))))) | |
| 1223 | 483 x⊆pxq : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → * x ⊆ ZFP p Q |
| 1222 | 484 x⊆pxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw |
| 485 ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where | |
| 486 ty21 : ZFProduct P Q (& (* (& < * a , * b >))) | |
| 1229 | 487 ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) |
| 1222 | 488 ty32 : ZFProduct P Q (& (* (& < * a , * b >))) |
| 489 ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx) | |
| 1229 | 490 (& (* (& < * a , * b >))) (subst (λ k → odef k |
| 1222 | 491 (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) |
| 1229 | 492 ty07 : odef (* x) (& < * a , * b >) |
| 1222 | 493 ty07 = xw |
| 494 ty08 : odef p a | |
| 1229 | 495 ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) |
| 1222 | 496 record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where |
| 497 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a | |
| 498 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 499 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
| 1223 | 500 p⊆P : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → p ⊆ P |
| 1222 | 501 p⊆P {x} {p} fx x=ψz {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw |
| 1229 | 502 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) |
| 1222 | 503 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) |
| 1169 | 504 FP : Filter {Power P} {P} (λ x → x) |
| 1218 | 505 FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where |
| 1213 | 506 ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q |
| 1215 | 507 ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 ) |
| 508 where | |
| 1222 | 509 -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fx) xy)) |
| 1213 | 510 -- x = ( px , qx ) , px ⊆ q |
| 511 ty03 : Power (ZFP P Q) ∋ ZFP q Q | |
| 512 ty03 z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) | |
| 1215 | 513 q⊆P : q ⊆ P |
| 514 q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) | |
| 1213 | 515 ty05 : filter F ∋ ZFP p Q |
| 1222 | 516 ty05 = filter1 F (λ z wz → isP→PxQ (p⊆P fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆pxq fx x=ψz) |
| 1213 | 517 ty06 : ZFP p Q ⊆ ZFP q Q |
| 518 ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq | |
| 1215 | 519 ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q |
| 520 ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq | |
| 1218 | 521 ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q) |
| 1222 | 522 ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } |
| 1229 | 523 record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq |
| 1219 | 524 = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where |
| 1220 | 525 ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q) |
| 1221 | 526 ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where |
| 527 pqz : odef (ZFP (p ∩ q) Q) z | |
| 528 pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz | |
| 1222 | 529 pqz1 : odef P (zπ1 pqz) |
| 530 pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz)) | |
| 531 pqz2 : odef Q (zπ2 pqz) | |
| 532 pqz2 = zp2 pqz | |
| 1229 | 533 ty53 : filter F ∋ ZFP p Q |
| 534 ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) | |
| 535 (subst (λ k → odef k z) *iso wz)) | |
| 1222 | 536 (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp) |
| 1229 | 537 ty52 : filter F ∋ ZFP q Q |
| 538 ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) | |
| 539 (subst (λ k → odef k z) *iso wz)) | |
| 1222 | 540 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq) |
| 1219 | 541 ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q ) |
| 1220 | 542 ty51 = filter2 F ty53 ty52 ty54 |
| 1219 | 543 ty50 : filter F ∋ ZFP (p ∩ q) Q |
| 1220 | 544 ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 |
| 1161 | 545 UFP : ultra-filter FP |
| 1223 | 546 UFP = record { proper = ty61 ; ultra = ty60 } where |
| 547 ty61 : ¬ (FPSet ∋ od∅) | |
| 1229 | 548 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where |
| 1223 | 549 ty63 : {x : Ordinal} → ¬ odef (* z) x |
| 550 ty63 {x} zx with x⊆pxq az x=ψz zx | |
| 551 ... | ab-pair xp xq = ¬x<0 xp | |
| 552 ty62 : odef (filter F) (& od∅) | |
| 553 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az | |
| 554 ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p)) | |
| 1229 | 555 ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} |
| 556 (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) | |
| 1226 | 557 (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) |
| 1223 | 558 ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp ) |
| 1224 | 559 ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp )) |
| 1169 | 560 uflp : UFLP TP FP UFP |
| 561 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP | |
| 1229 | 562 |
| 563 -- FPSet is in Projection ⁻¹ F | |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
564 FPSet⊆F : {x : Ordinal } → odef FPSet x → odef (filter F) (& (ZFP (* x) Q)) |
| 1233 | 565 FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where |
| 1231 | 566 Rx : HOD |
| 567 Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) | |
| 568 RxQ∋z : * z ⊆ ZFP Rx Q | |
| 1235 | 569 RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl } (zp2 b )) where |
| 1232 | 570 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) |
| 571 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ) | |
| 1235 | 572 ty73 : & (* (zπ1 a)) ≡ zπ1 b |
| 573 ty73 = begin | |
| 574 & (* (zπ1 a)) ≡⟨ &iso ⟩ | |
| 575 zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ | |
| 576 zπ1 b ∎ where open ≡-Reasoning | |
| 577 ty70 : & < * (& (* (zπ1 a))) , * (zπ2 b) > ≡ w | |
| 578 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) | |
| 579 ... | eq = trans (cong₂ (λ j k → & < * j , k > ) ty73 refl ) (trans eq &iso ) | |
| 1231 | 580 ty71 : * z ⊆ ZFP (* x) Q |
| 581 ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where | |
| 582 ty72 : Rx ≡ * x | |
| 583 ty72 = begin | |
| 584 Rx ≡⟨ sym *iso ⟩ | |
| 585 * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩ | |
| 586 * x ∎ where open ≡-Reasoning | |
| 1233 | 587 ty80 : Power (ZFP P Q) ∋ ZFP (* x) Q |
| 588 ty80 y yx = isP→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where | |
| 589 ty81 : * x ⊆ P | |
| 590 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw | |
| 1235 | 591 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym ty84) ty87 where |
| 592 a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) | |
| 593 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1)) | |
| 594 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 ) | |
| 595 ty87 : odef P (zπ1 b) | |
| 596 ty87 = zp1 b | |
| 597 ty84 : w ≡ (zπ1 b) | |
| 598 ty84 = begin | |
| 599 w ≡⟨ trans x=ψz1 &iso ⟩ | |
| 600 zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩ | |
| 601 zπ1 b ∎ where open ≡-Reasoning | |
| 1154 | 602 |
| 1227 | 603 -- copy and pasted, sorry |
| 604 -- | |
| 1229 | 605 isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q |
| 606 isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) | |
| 607 fx→qx : {x : HOD } → filter F ∋ x → HOD | |
| 1225 | 608 fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) |
| 609 fx→qx1 : {q : HOD } {p : Ordinal } → odef P p → (fq : filter F ∋ ZFP P q ) → fx→qx fq ≡ q | |
| 610 fx→qx1 {q} {p} qq fq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where | |
| 611 ty21 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → ZFProduct P Q (& (* (& < * a , * b >))) | |
| 1229 | 612 ty21 qz pz = F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz )) |
| 1225 | 613 ty32 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → zπ2 (ty21 qz pz) ≡ b |
| 614 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where | |
| 615 ty33 : {a b x : Ordinal } ( q : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 q ≡ b | |
| 616 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 617 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) | |
| 618 ty20 : {x : Ordinal} → odef (fx→qx fq) x → odef q x | |
| 619 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef q k) b=x qz where | |
| 1229 | 620 ty24 : * x ≡ * b |
| 1225 | 621 ty24 = begin |
| 622 * x ≡⟨ cong (*) x=ψz ⟩ | |
| 623 _ ≡⟨ *iso ⟩ | |
| 624 * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 qz pz) ⟩ | |
| 625 * b ∎ where open ≡-Reasoning | |
| 1229 | 626 b=x : b ≡ x |
| 1225 | 627 b=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) |
| 1229 | 628 ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x |
| 1226 | 629 ty22 {x} qx = record { z = _ ; az = ab-pair qq qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where |
| 1225 | 630 ty12 : * x ≡ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) |
| 631 ty12 = begin | |
| 632 * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩ | |
| 633 * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ∎ where open ≡-Reasoning | |
| 634 FQSet : HOD | |
| 635 FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) ))) | |
| 636 FQSet∋zpq : {q : HOD} → q ⊆ Q → filter F ∋ ZFP P q → FQSet ∋ q | |
| 637 FQSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where | |
| 638 -- brain damaged one | |
| 1229 | 639 ty11 : {y : HOD} {xy : (* (& (ZFP P q ))) ∋ y } → |
| 1225 | 640 * (zπ2 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ2 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) |
| 641 ty11 {y} {xy} = cong (λ k → * (zπ2 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where | |
| 642 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy | |
| 1229 | 643 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) |
| 1225 | 644 ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q |
| 645 ty10 = begin | |
| 1229 | 646 Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) |
| 647 ≡⟨ | |
| 1225 | 648 cong (λ k → Replace' (* (& (ZFP P q ))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) |
| 649 ⟩ | |
| 1229 | 650 Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) |
| 1225 | 651 ≡⟨ Replace'-iso _ ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ⟩ |
| 1229 | 652 Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ |
| 1226 | 653 fx→qx fq ≡⟨ fx→qx1 ap fq ⟩ |
| 1225 | 654 q ∎ where open ≡-Reasoning |
| 655 FQSet⊆PP : FQSet ⊆ Power Q | |
| 656 FQSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw | |
| 1229 | 657 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } |
| 658 = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) | |
| 1225 | 659 (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) |
| 660 X=F2 : (x : Ordinal) (q : HOD) (fx : odef (filter F) x) → Set n | |
| 661 X=F2 x q fx = & q ≡ & (Replace' (* x) (λ y xy → | |
| 662 * (zπ2 (f⊆L F | |
| 663 (subst (odef (filter F)) (sym &iso) fx) | |
| 664 (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy))))) | |
| 665 x⊆qxq : {x : Ordinal} {q : HOD} (fx : odef (filter F) x) → X=F2 x q fx → * x ⊆ ZFP P q | |
| 666 x⊆qxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw | |
| 667 ... | ab-pair {a} {b} pw qw = ab-pair pw ty08 where | |
| 668 ty21 : ZFProduct P Q (& (* (& < * a , * b >))) | |
| 1229 | 669 ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) |
| 1225 | 670 ty32 : ZFProduct P Q (& (* (& < * a , * b >))) |
| 671 ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx) | |
| 1229 | 672 (& (* (& < * a , * b >))) (subst (λ k → odef k |
| 1225 | 673 (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) |
| 1229 | 674 ty07 : odef (* x) (& < * a , * b >) |
| 1225 | 675 ty07 = xw |
| 676 ty08 : odef p b | |
| 1229 | 677 ty08 = subst (λ k → odef k b ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) |
| 1225 | 678 record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where |
| 679 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b | |
| 680 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
| 681 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) | |
| 1226 | 682 q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ Q |
| 1225 | 683 q⊆Q {x} {p} fx x=ψz {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw |
| 1229 | 684 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) |
| 1226 | 685 (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) |
| 1169 | 686 FQ : Filter {Power Q} {Q} (λ x → x) |
| 1225 | 687 FQ = record { filter = FQSet ; f⊆L = FQSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where |
| 688 ty01 : {p q : HOD} → Power Q ∋ q → FQSet ∋ p → p ⊆ q → FQSet ∋ q | |
| 1229 | 689 ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq q⊆P (ty10 ty05 ty06 ) |
| 1225 | 690 where |
| 1226 | 691 -- p ≡ (Replace' (* x) (λ y xy → (zπ2 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy)) |
| 692 -- x = ( px , qx ) , qx ⊆ q | |
| 1229 | 693 ty03 : Power (ZFP P Q) ∋ ZFP P q |
| 694 ty03 z zpq = isQ→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) | |
| 1225 | 695 q⊆P : q ⊆ Q |
| 696 q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) | |
| 697 ty05 : filter F ∋ ZFP P p | |
| 1226 | 698 ty05 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆qxq fx x=ψz) |
| 1229 | 699 ty06 : ZFP P p ⊆ ZFP P q |
| 700 ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) | |
| 701 ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q | |
| 1225 | 702 ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq |
| 703 ty02 : {p q : HOD} → FQSet ∋ p → FQSet ∋ q → Power Q ∋ (p ∩ q) → FQSet ∋ (p ∩ q) | |
| 704 ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } | |
| 1229 | 705 record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq |
| 1226 | 706 = FQSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where |
| 707 ty54 : Power (ZFP P Q) ∋ (ZFP P p ∩ ZFP P q ) | |
| 1225 | 708 ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where |
| 709 pqz : odef (ZFP P (p ∩ q) ) z | |
| 1226 | 710 pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz |
| 1225 | 711 pqz1 : odef P (zπ1 pqz) |
| 712 pqz1 = zp1 pqz | |
| 713 pqz2 : odef Q (zπ2 pqz) | |
| 1226 | 714 pqz2 = q⊆Q fzp x=ψzp (proj1 (zp2 pqz)) |
| 1229 | 715 ty53 : filter F ∋ ZFP P p |
| 716 ty53 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzp x=ψzp) | |
| 717 (subst (λ k → odef k z) *iso wz)) | |
| 1226 | 718 (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp) |
| 1229 | 719 ty52 : filter F ∋ ZFP P q |
| 720 ty52 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) | |
| 721 (subst (λ k → odef k z) *iso wz)) | |
| 1226 | 722 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq) |
| 723 ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q ) | |
| 724 ty51 = filter2 F ty53 ty52 ty54 | |
| 1229 | 725 ty50 : filter F ∋ ZFP P (p ∩ q) |
| 1226 | 726 ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51 |
| 1166 | 727 UFQ : ultra-filter FQ |
| 1225 | 728 UFQ = record { proper = ty61 ; ultra = ty60 } where |
| 729 ty61 : ¬ (FQSet ∋ od∅) | |
| 1229 | 730 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where |
| 1225 | 731 ty63 : {x : Ordinal} → ¬ odef (* z) x |
| 732 ty63 {x} zx with x⊆qxq az x=ψz zx | |
| 733 ... | ab-pair xp xq = ¬x<0 xq | |
| 734 ty62 : odef (filter F) (& od∅) | |
| 735 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az | |
| 736 ty60 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (FQSet ∋ p) ∨ (FQSet ∋ (Q ＼ p)) | |
| 1229 | 737 ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q} |
| 738 (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) | |
| 1226 | 739 (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) |
| 1225 | 740 ... | case1 fq = case1 (FQSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fq ) |
| 741 ... | case2 fnp = case2 (FQSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj2 ZFP\Q)) fnp )) | |
| 742 | |
| 1229 | 743 |
| 744 -- FQSet is in Projection ⁻¹ F | |
| 745 FQSet⊆F : {x : Ordinal } → odef FQSet x → odef (filter F) (& (ZFP P (* x) )) | |
| 1236 | 746 FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where |
| 747 Rx : HOD | |
| 748 Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) | |
| 749 PxRx∋z : * z ⊆ ZFP P Rx | |
| 750 PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) where | |
| 751 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) | |
| 752 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ) | |
| 753 ty73 : & (* (zπ2 a)) ≡ zπ2 b | |
| 754 ty73 = begin | |
| 755 & (* (zπ2 a)) ≡⟨ &iso ⟩ | |
| 756 zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ | |
| 757 zπ2 b ∎ where open ≡-Reasoning | |
| 758 ty70 : & < * (zπ1 b) , * (& (* (zπ2 a))) > ≡ w | |
| 759 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) | |
| 760 ... | eq = trans (cong₂ (λ j k → & < j , * k > ) refl ty73 ) (trans eq &iso ) | |
| 761 ty71 : * z ⊆ ZFP P (* x) | |
| 762 ty71 = subst (λ k → * z ⊆ ZFP P k ) ty72 PxRx∋z where | |
| 763 ty72 : Rx ≡ * x | |
| 764 ty72 = begin | |
| 765 Rx ≡⟨ sym *iso ⟩ | |
| 766 * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩ | |
| 767 * x ∎ where open ≡-Reasoning | |
| 768 ty80 : Power (ZFP P Q) ∋ ZFP P (* x) | |
| 769 ty80 y yx = isQ→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where | |
| 770 ty81 : * x ⊆ Q | |
| 771 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw | |
| 772 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym ty84) ty87 where | |
| 773 a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) | |
| 774 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1)) | |
| 775 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 ) | |
| 776 ty87 : odef Q (zπ2 b) | |
| 777 ty87 = zp2 b | |
| 778 ty84 : w ≡ (zπ2 b) | |
| 779 ty84 = begin | |
| 780 w ≡⟨ trans x=ψz1 &iso ⟩ | |
| 781 zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩ | |
| 782 zπ2 b ∎ where open ≡-Reasoning | |
| 783 | |
| 1229 | 784 |
| 1169 | 785 uflq : UFLP TQ FQ UFQ |
| 786 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ | |
| 1154 | 787 |
| 1166 | 788 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
| 1229 | 789 Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq) |
| 790 | |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
791 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v |
| 1229 | 792 isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (subst (λ k → odef k z) *iso xz)) |
| 793 (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb b∋l )) bpq⊆v where | |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
794 -- |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
795 -- Product Topolgy's open set contains a subbase which is an element of ZPF p Q or ZPF P q |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
796 -- Neighbor of limit contains an open set which conatins a limit |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
797 -- every point of an open set is covered by a subbase |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
798 -- so there is a subbase which contains a limit, the subbase is an element of projection of a filter (P or Q) |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
799 TPQ = ProductTopology TP TQ |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
800 lim = & < * (UFLP.limit uflp) , * (UFLP.limit uflq) > |
| 1229 | 801 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u nei) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
| 802 bpq = Neighbor.ou nei (Neighbor.ux nei) | |
| 803 b∋l : odef (* (Base.b bpq)) lim | |
| 804 b∋l = Base.bx bpq | |
| 1172 | 805 pqb : Subbase (pbase TP TQ) (Base.b bpq ) |
|
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
806 pqb = Base.sb bpq |
| 1229 | 807 pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u nei ) |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
808 bpq⊆v : * (Base.b bpq) ⊆ * v |
| 1229 | 809 bpq⊆v {x} bx = Neighbor.u⊆v nei (pqb⊆opq bx) |
| 1173 | 810 pqb⊆opq = Base.b⊆u bpq |
| 1229 | 811 F∋base : {b : Ordinal } → Subbase (pbase TP TQ) b → odef (* b) lim → odef (filter F) b |
| 812 F∋base {b} (gi (case1 px)) bl = subst (λ k → odef (filter F) k) (sym (BaseP.prod px)) f∋b where | |
| 813 -- | |
| 814 -- subbase of product topology which includes lim is in FP, so in F | |
| 815 -- | |
| 816 isl00 : odef (ZFP (* (BaseP.p px)) Q) lim | |
| 817 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) *iso ) bl | |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
818 px∋limit : odef (* (BaseP.p px)) (UFLP.limit uflp) |
| 1229 | 819 px∋limit = isl01 isl00 refl where |
| 820 isl01 : {x : Ordinal } → odef (ZFP (* (BaseP.p px)) Q) x → x ≡ lim → odef (* (BaseP.p px)) (UFLP.limit uflp) | |
| 821 isl01 (ab-pair {a} {b} bx qx) ab=lim = subst (λ k → odef (* (BaseP.p px)) k) a=lim bx where | |
| 822 a=lim : a ≡ UFLP.limit uflp | |
| 823 a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) | |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
824 fp∋b : filter FP ∋ * (BaseP.p px) |
| 1229 | 825 fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
826 ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x } |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
827 f∋b : odef (filter F) (& (ZFP (* (BaseP.p px)) Q)) |
|
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
828 f∋b = FPSet⊆F (subst (λ k → odef (filter FP) k ) &iso fp∋b ) |
| 1229 | 829 F∋base {b} (gi (case2 qx)) bl = subst (λ k → odef (filter F) k) (sym (BaseQ.prod qx)) f∋b where |
| 830 isl00 : odef (ZFP P (* (BaseQ.q qx))) lim | |
| 831 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) *iso ) bl | |
| 832 qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq) | |
| 833 qx∋limit = isl01 isl00 refl where | |
| 834 isl01 : {x : Ordinal } → odef (ZFP P (* (BaseQ.q qx)) ) x → x ≡ lim → odef (* (BaseQ.q qx)) (UFLP.limit uflq) | |
| 835 isl01 (ab-pair {a} {b} px bx) ab=lim = subst (λ k → odef (* (BaseQ.q qx)) k) b=lim bx where | |
| 836 b=lim : b ≡ UFLP.limit uflq | |
| 837 b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) | |
| 838 fp∋b : filter FQ ∋ * (BaseQ.q qx) | |
| 839 fp∋b = UFLP.is-limit uflq record { u = _ ; ou = BaseQ.oq qx ; ux = qx∋limit | |
| 840 ; v⊆P = λ {x} lt → os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) (BaseQ.oq qx)) lt ; u⊆v = λ x → x } | |
| 841 f∋b : odef (filter F) (& (ZFP P (* (BaseQ.q qx)) )) | |
| 842 f∋b = FQSet⊆F (subst (λ k → odef (filter FQ) k ) &iso fp∋b ) | |
| 843 F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where | |
| 844 -- filter contains finite intersection | |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
845 fb01 : odef (filter F) x |
| 1229 | 846 fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl)) |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
847 fb02 : odef (filter F) y |
| 1229 | 848 fb02 = F∋base b2 (proj2 (subst (λ k → odef k lim) *iso bl)) |
|
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1227
diff
changeset
|
849 F∋x∩y : odef (filter F) (& (* x ∩ * y)) |
| 1229 | 850 F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02) |
| 851 (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01)) | |
| 852 (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb02))) | |
| 1154 | 853 |
| 1170 | 854 |
| 855 | |
| 856 | |
| 857 | |
| 858 |