---

Step * 1 of Lemma fpf-restrict-dom


∀A:Type. ∀eq:EqDecider(A). ∀B:A ─→ Type. ∀f:x:A fp-> B[x]. ∀P:A ─→ 𝔹. ∀x:A.
  (↑x ∈ dom(fpf-restrict(f;P)) ⇐⇒ {(↑x ∈ dom(f)) ∧ (↑(P x))})
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `guard` 0
   THEN (RWO "member-fpf-domain" 0 THENM Reduce 0 THENM RWO "member_filter" 0)
   THEN Auto) }

---

Latex:



\mforall{}A:Type.  \mforall{}eq:EqDecider(A).  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}f:x:A  fp->  B[x].  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:A.
    (\muparrow{}x  \mmember{}  dom(fpf-restrict(f;P))  \mLeftarrow{}{}\mRightarrow{}  \{(\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}(P  x))\})


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `guard`  0
  THEN  (RWO  "member-fpf-domain"  0  THENM  Reduce  0  THENM  RWO  "member\_filter"  0)
  THEN  Auto)

---

Home Index