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

comparison src/Tychonoff.agda @ 1187:d996fe8dd116

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Feb 2023 01:19:24 +0900
parents 7d2bae0ff36b
children 8cbc3918d875
comparison
equal deleted inserted replaced
1186:ffe5bc98f9d1 1187:d996fe8dd116
66 -- P is empty 66 -- P is empty
67 fip02 : {x : Ordinal } → ¬ odef P x 67 fip02 : {x : Ordinal } → ¬ odef P x
68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) ) 68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
69 ... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where 69 ... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where
70 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 70 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
71 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x 71 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
72 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD 72 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
73 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) 73 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
74 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } 74 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) }
75 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P 75 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
76 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb 76 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb
160 CF⊆CS : CF ⊆ CS TP 160 CF⊆CS : CF ⊆ CS TP
161 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)) 161 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))
162 -- 162 --
163 -- it is set of closed set and has FIP ( F is proper ) 163 -- it is set of closed set and has FIP ( F is proper )
164 -- 164 --
165 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x 165 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
166 ufl01 = ? 166 ufl01 = ?
167 -- 167 --
168 -- so we have a limit 168 -- so we have a limit
169 -- 169 --
170 limit : Ordinal 170 limit : Ordinal
243 nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b 243 nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b
244 nproper = ? 244 nproper = ?
245 b∋z : odef nei1 z 245 b∋z : odef nei1 z
246 b∋z = ? 246 b∋z = ?
247 bp : BaseP {P} TP Q z 247 bp : BaseP {P} TP Q z
248 bp = record { b = ? ; op = ? ; prod = ? } 248 bp = record { p = ? ; op = ? ; prod = ? }
249 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 249 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
250 neip = ? 250 neip = ?
251 il2 : * z ⊆ ZFP (Power P) (Power Q) 251 il2 : * z ⊆ ZFP (Power P) (Power Q)
252 il2 = ? 252 il2 = ?
253 il3 : filter F ∋ ? 253 il3 : filter F ∋ ?