Members/kono/Proof/ZF-in-agda: src/Tychonoff.agda comparison

comparison src/Tychonoff.agda @ 1211:f17d060e0bda

UFLP→FIP FIP→UFLP with Zorn done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 04 Mar 2023 11:39:46 +0900
parents	806109d79562
children	22de2d4f7271

comparison

equal deleted inserted replaced

-:806109d79562
+:f17d060e0bda
 open ODC O
 open import filter O
 open import OPair O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 open Filter
 open Topology
 -- FIP is UFL
 -- filter Base
 record FBase (P : HOD ) (X : Ordinal ) (u : Ordinal) : Set n where
 record UFLP {P : HOD} (TP : Topology P)  (F : Filter {Power P} {P} (λ x → x) )
 (ultra : ultra-filter F ) : Set (suc (suc n)) where
 field
 limit : Ordinal
 P∋limit : odef P limit
-is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F
+is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)
 UFLP→FIP : {P : HOD} (TP : Topology P) →
 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp with trio< (& P) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
 N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
 -- filter base is not empty necessary for generating ultra filter
 nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
 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
 N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP)
 → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
 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
 e : HOD  -- we have an element of X
 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
 Xe : odef (* X) (& e)
 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
 nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) )
 nn02 : * (& (nc 0<X CSX fip)) ⊆ P
 nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
 0<PP : o∅ o< & (Power P)
 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
 --
 -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x )
 --
 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅)
 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
 x≤0 : x o< osuc  o∅
 x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u))
 fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x
 fp00 b y b<X (gi by ) = gi ( b<X by )
 fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz)
 --
 -- then we have maximum ultra filter
 --
-maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
+maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-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)
+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)
-mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
+mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
-mf {X} CSX fp =  MaximumFilter.mf (maxf CSX fp)
+mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
-ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
+ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-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)
+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)
 --
 -- so i has a limit as a limit of UIP
 --
 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
 limit {X} CSX fp with trio< o∅ X
-... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))
+... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))
 ... | tri≈ ¬a 0=X ¬c = o∅
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 --
 -- the limit is an limit of entire elements of X
 --
 uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
 uf01 {X} CSX fp {x} xx with trio< o∅ X
 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx )))
-... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp))}
+... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))}
-(UFLP.P∋limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)))
+(UFLP.P∋limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)))
 ... | case1 lt = lt -- odef (* x) y
-... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf CSX fp) uf11 ) where
+... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where
-y = UFLP.limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp))
+y = UFLP.limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))
 x⊆P : * x ⊆ P
 x⊆P = cs⊆L TP (CSX (subst (λ k → odef (* X) k) (sym &iso) xx))
 uf10 : odef (P ＼ * x ) y
 uf10 = nlxy
 uf03 : Neighbor TP y (& (P ＼ * x ))
 uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx))
 ; ux = subst (λ k → odef k y) (sym *iso) uf10
 ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
 ; u⊆v = λ x → x  }
 uf07 : * (& (* x , * x)) ⊆ * X
 uf07 {y} lt with subst (λ k → odef k y) *iso lt
 ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
 ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
-uf05 : odef (filter (MaximumFilter.mf (maxf CSX fp))) x
+uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x
-uf05 = MaximumFilter.F⊆mf (maxf CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
+uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
 ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  ; u⊆P = x⊆P ; x⊆u = λ x → x  }
-uf06 : odef (filter (MaximumFilter.mf (maxf CSX fp))) (& (P ＼ * x ))
+uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x ))
-uf06 = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) uf03 (subst (λ k → odef k y) (sym *iso) uf10)
+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  )
 uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
 uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
 uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y
 uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy )
 uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x )))
 uf12 z pz with subst (λ k → odef k z) *iso pz
 ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz
-uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅
+uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅
-uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13
+uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅))
-( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12  )
+( 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  )
 x⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → x ⊆ Cl TP x
 x⊆Clx {P} TP {x}  x<p {y} xy  = ⟪ x<p xy , (λ c csc x<c → x<c xy )  ⟫
 P⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → Cl TP x ⊆ P
 P⊆Clx {P} TP {x}  x<p {y} xy  = proj1 xy
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
 →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
 ; P∋limit = ufl10 ; is-limit = ufl00 } where
 F∋P : odef (filter F) (& P)
 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 ) )
 ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp )
 ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
 fl20 :  (P ＼ Ord o∅) =h=  P
 fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  }
 0<P : o∅ o< & P
 0<P with trio< o∅ (& P)
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋P) )
 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 -- take closure of given filter elements
 --
 CF : HOD
 CF = Replace (filter F) (λ x → Cl TP x  )
 CF⊆CS : CF ⊆ CS TP
 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))
 --
 -- it is set of closed set and has FIP ( F is proper )
 --
 ufl08  : {z : Ordinal} → odef (Power P) (& (Cl TP (* z)))
 ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw
 F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x
 F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where
 ufl09 : * z ⊆ P
 ufl09 {y} zy = f⊆L F az _ zy
 ufl07 : odef (filter F) x
 ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso))  ufl08  )
 (subst (λ k → odef (filter F) k) (sym &iso) az)
 (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) ))
 F∋sb  (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx))
 (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy))
 (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) )))
 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
 ufl01 {x} sb = ufl04  where
 ufl04 : o∅ o< x
 ufl04 with trio< o∅ x
 ... | tri< a ¬b ¬c = a
 ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) (
 begin
 x  ≡⟨ sym b ⟩
 o∅ ≡⟨ sym ord-od∅ ⟩
 & od∅  ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) ))  where open ≡-Reasoning
 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01)
 ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11  where
 ufl11 : odef (* (& CF)) (& P)
 ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az  = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP)))   }
 --
 -- so we have a limit
 --
 limit : Ordinal
 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
 --
 -- Neigbor of limit ⊆ Filter
 --
 -- if odef (* X) x, Cl TP x contains limit (ufl02)
 -- in (nei : Neighbor TP limit v) , there is an open Set u which contains the limit
 -- F contains u or P ＼ u because F is ultra
 --   if F ∋ u, then F ∋ v from u ⊆ v which is a propetery of Neighbor
 --   if F ∋ P ＼ u, it is a closed set (Cl (P ＼ u) ≡ P ＼ u) and it does not contains the limit
 --      this contradicts ufl02
 pp :  {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei))
 pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz
 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz )
-ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F
+ufl00 :  {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v
-ufl00 {v} nei {x} vx with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei ))
+ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei ))
-... | case1 fu = ? where -- Neighbor.u⊆v nei ? where
+... | case1 fu = subst (λ k → odef (filter F) k) &iso
--- subst (λ k → odef (filter F) k) &iso ( filter1 F ? ? ? ) where
+( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px)  fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where
-px : Power P ∋ * x
+u = * (Neighbor.u nei)
-px z xz = Neighbor.v⊆P nei ?
+px : Power P ∋ * v
+px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz )
 ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where
 u = * (Neighbor.u nei)
 P\u : HOD
 P\u = P ＼ u
 P\u∋limit : odef P\u limit
 P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where
 ufl04 : & P\u ≡ & (Cl TP (* (& P\u)))
 ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso)
 (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) )))))
 ufl03 : odef CF (& P\u )
 ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 }
 ¬P\u∋limit : ¬ odef P\u limit
 ¬P\u∋limit ⟪ Pl , nul ⟫ = nul ( Neighbor.ux nei )
 uflq : UFLP TQ FQ UFQ
 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
 Pf = ?
 pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F
 pq⊆F = ?
-isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F
+isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v
-isL {v} npq {x} fx = ? where
+isL {v} npq = ? where
 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
 bpq = Neighbor.ou npq (Neighbor.ux npq)
 pqb : Subbase (pbase TP TQ) (Base.b bpq )
 pqb = Base.sb bpq
 pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq )
 pqb⊆opq = Base.b⊆u bpq
 base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆  * (Neighbor.u npq) → * b ⊆ filter F
 base⊆F (gi (case1 px)) b⊆u {z} bz = fz  where
 -- F contains no od∅, because it projection contains no od∅
 --    x is an element of BaseP, which is a subset of Neighbor npq
 --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
 --    BaseP ∩ F is not empty
 --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F ,
 il1 : odef (Power P) z ∧ ZProj1 (filter F) z
-il1 = UFLP.is-limit uflp ? bz
+il1 = ? -- UFLP.is-limit uflp ? bz
 nei1 : HOD
 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
 plimit : Ordinal
 plimit = UFLP.limit uflp
 nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
 nproper = ?
 b∋z : odef nei1 z
 b∋z = ?
 bp : BaseP {P} TP Q z
 bp = record { p = ? ; op = ? ; prod = ? }
 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
 neip = ?
 il2 : * z ⊆ ZFP (Power P) (Power Q)
 il2 = ?
 il3 : filter F ∋ ?
 il3 = ?
 fz : odef (filter F) z
 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)
 base⊆F (gi (case2 qx)) b⊆u {z} bz = ?
 base⊆F (g∩ b1 b2) b⊆u {z} bz = ?

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

comparison src/Tychonoff.agda @ 1211:f17d060e0bda