Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/Tychonoff.agda @ 1208:151f4c971a50
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Mar 2023 19:44:29 +0900 |
parents | 56d501cf0318 |
children | 09e4b32ece2e |
line wrap: on
line source
{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Ordinals module Tychonoff {n : Level } (O : Ordinals {n}) where open import zf open import logic open _∧_ open _∨_ open Bool import OD open import Relation.Nullary open import Data.Empty open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality import BAlgebra open BAlgebra O open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom import OrdUtil import ODUtil open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal open Ordinals.IsNext isNext open OrdUtil O open ODUtil O import ODC open ODC O open import filter O open import OPair O open import Topology 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 field b x : Ordinal b⊆X : * b ⊆ * X sb : Subbase (* b) x u⊆P : * u ⊆ P x⊆u : * x ⊆ * u 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 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 ) ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where -- P is empty fip02 : {x : Ordinal } → ¬ odef P x fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) ) fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} → odef (* X) x → odef (* x) o∅ -- empty P case -- if 0 < X then 0 < x ∧ P ∋ xfrom fip -- if 0 ≡ X then ¬ odef X x fip03 {X} CX fip {x} xx with trio< o∅ X ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where 0<x : o∅ o< x 0<x = fip (gi xx ) 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) ) ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin * X ≡⟨ cong (*) (sym 0=X) ⟩ * o∅ ≡⟨ o∅≡od∅ ⟩ od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = uf01 } where fip : {X : Ordinal} → * X ⊆ CS TP → Set n fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } 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 nn00 : odef (Power P) o∅ nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt ... | x<0 = ⊥-elim ( ¬x<0 x<0) -- -- FIP defines a filter -- F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where f10 : q ⊆ P f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) 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 p∩q⊆p : * (& (p ∩ q)) ⊆ P p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) f20 : * (& Np+Nq) ⊆ * X f20 {x} npq with subst (λ k → odef k x) *iso npq ... | case1 np = FBase.b⊆X Np np ... | case2 nq = FBase.b⊆X Nq nq 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} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp) ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 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) -- -- 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≈ ¬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))} (UFLP.P∋limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))) ... | case1 lt = lt -- odef (* x) y ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf CSX fp) uf11 ) where y = UFLP.limit ( uflp ( mf 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 = MaximumFilter.F⊆mf (maxf 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 = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp)) uf03 (subst (λ k → odef k y) (sym *iso) uf10) 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 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 ( filter2 (MaximumFilter.mf (maxf CSX fp)) 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 = ? ; is-limit = ufl00 } where -- -- 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 ... | t = proj1 t fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz ) 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) -- -- 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 -- ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF ufl03 {f} {v} ff nei fv=0 = ? pp : {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x) pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = v⊆P ? ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx)) ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv ... | case2 nfv = ? -- will contradicts ufl03 -- product topology of compact topology is compact Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F) → UFLP TP F UF uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) → UFLP TQ F UF uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF -- Product of UFL has a limit point uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) F UF uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where FP : Filter {Power P} {P} (λ x → x) FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where ty00 : Proj1 (filter F) (Power P) (Power Q) ⊆ Power P ty00 {x} ⟪ PPx , ppf ⟫ = PPx UFP : ultra-filter FP UFP = record { proper = ? ; ultra = ? } uflp : UFLP TP FP UFP uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP FQ : Filter {Power Q} {Q} (λ x → x) FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where ty00 : Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q ty00 {x} ⟪ QPx , ppf ⟫ = QPx UFQ : ultra-filter FQ UFQ = record { proper = ? ; ultra = ? } 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} npq {x} fx = ? 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 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 = ?