---

Step * of Lemma fpf-restrict-cap

∀[A:Type]. ∀[P:A ─→ 𝔹]. ∀[x:A].
  ∀[f:x:A fp-> Top]. ∀[eq:EqDecider(A)]. ∀[z:Top].  (fpf-restrict(f;P)(x)?z ~ f(x)?z) supposing ↑(P x)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``fpf-cap`` 0 THEN EqCD THEN Try (Trivial)) }

1
1. A : Type
2. P : A ─→ 𝔹
3. x : A
4. ↑(P x)
5. f : x:A fp-> Top
6. eq : EqDecider(A)
7. z : Top
⊢ x ∈ dom(fpf-restrict(f;P)) ~ x ∈ dom(f)

---

Latex:


\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:A].
    \mforall{}[f:x:A  fp->  Top].  \mforall{}[eq:EqDecider(A)].  \mforall{}[z:Top].    (fpf-restrict(f;P)(x)?z  \msim{}  f(x)?z) 
    supposing  \muparrow{}(P  x)


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``fpf-cap``  0  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index