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

comparison src/Tychonoff.agda @ 1204:4d894c166762

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 03 Mar 2023 08:37:02 +0800
parents 2f09ce1dd2a1
children 83ac320583f8
comparison
equal deleted inserted replaced
1203:2f09ce1dd2a1 1204:4d894c166762
83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin 83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
84 * X ≡⟨ cong (*) (sym 0=X) ⟩ 84 * X ≡⟨ cong (*) (sym 0=X) ⟩
85 * o∅ ≡⟨ o∅≡od∅ ⟩ 85 * o∅ ≡⟨ o∅≡od∅ ⟩
86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning 86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = ? } where 88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = uf01 } where
89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x 90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) }
94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P 94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb 95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb
96 -- filter base is not empty 96 -- filter base is not empty
97 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD 97 nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
98 nc {X} CSX fip with trio< o∅ X 98 nc {X} 0<X CSX fip = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where
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 99 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) ) 100 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
102 Xe : odef (* X) (& e) 101 Xe : odef (* X) (& e)
103 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 102 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
104 ... | tri≈ ¬a b ¬c = od∅ 103 N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP)
105 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 104 → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
106 N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc CSX fip) ) 105 N∋nc {X} 0<X CSX fip = record { b = ? ; x = ? ; b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where
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 106 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) ) 107 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
111 Xe : odef (* X) (& e) 108 Xe : odef (* X) (& e)
112 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 109 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))) ) 110 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 )
116 0<PP : o∅ o< & (Power P) 111 0<PP : o∅ o< & (Power P)
117 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where 112 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∅ 113 nn00 : odef (Power P) o∅
119 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt 114 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt
120 ... | x<0 = ⊥-elim ( ¬x<0 x<0) 115 ... | x<0 = ⊥-elim ( ¬x<0 x<0)
154 -- 149 --
155 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) 150 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
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) 151 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)
157 mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) 152 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) 153 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) 154 ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
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) 155 ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
161 -- 156 --
162 -- so i has a limit as a limit of UIP 157 -- so i has a limit as a limit of UIP
163 -- 158 --
164 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal 159 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
165 limit {X} CSX fp with trio< o∅ X 160 limit {X} CSX fp with trio< o∅ X
166 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) 161 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))
167 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin 162 ... | tri≈ ¬a 0=X ¬c = o∅
168 * X ≡⟨ cong (*) (sym 0=X) ⟩
169 * o∅ ≡⟨ o∅≡od∅ ⟩
170 od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
171 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 163 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
172 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 164 uf02 : {X v : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX)
173 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp ) 165 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp )
174 uf02 {X} {v} CSX fp nei {x} vx with trio< o∅ X 166 uf02 {X} {v} 0<X CSX fp nei {x} vx with trio< o∅ X
175 ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx 167 ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp)) nei vx
176 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin 168 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a 0<X )
177 * X ≡⟨ cong (*) (sym 0=X) ⟩
178 * o∅ ≡⟨ o∅≡od∅ ⟩
179 od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
180 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 169 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
181 -- 170 --
182 -- the limit is an limit of entire elements of X 171 -- the limit is an limit of entire elements of X
183 -- 172 --
184 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) 173 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
185 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp)) 174 uf01 {X} CSX fp {x} xx with trio< o∅ X
186 ... | yes y = subst (λ k → odef (* x) k) &iso y 175 ... | tri< 0<X ¬b ¬c = ?
187 ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 ) where 176 ... | tri≈ ¬a 0=X ¬c = ?
188 uf03 : OS TP ∋ ( P ＼ (* x)) 177 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
189 uf03 = ?
190 uf05 : odef ( P ＼ (* x)) (limit CSX fp)
191 uf05 = ⟪ ? , subst (λ k → ¬ odef (* x) k) ? nxl ⟫
192 uf04 : Neighbor TP (limit CSX fp) (& ( P ＼ (* (limit CSX fp))))
193 uf04 = record { u = & ( P ＼ (* x)) ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ? }
194 uf07 : odef (filter (mf CSX fp)) x
195 uf07 = ?
196 uf06 : odef (filter (mf CSX fp)) (& ( P ＼ (* x)) )
197 uf06 = ?
198 uf08 : (filter (mf CSX fp)) ∋ od∅
199 uf08 = ?
200
201 178
202 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP 179 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
203 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF 180 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
204 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 181 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
205 -- 182 --