---

Step * of Lemma domain_fpf_restrict_lemma

∀P,f:Top.  (fpf-domain(fpf-restrict(f;P)) ~ filter(P;fpf-domain(f)))
BY
{ (UnivCD THENA Auto) }

1
1. P : Top@i
2. f : Top@i
⊢ fpf-domain(fpf-restrict(f;P)) ~ filter(P;fpf-domain(f))

---

Latex:


\mforall{}P,f:Top.    (fpf-domain(fpf-restrict(f;P))  \msim{}  filter(P;fpf-domain(f)))


By

(UnivCD  THENA  Auto)

---

Home Index