---

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
{ xxx((UnivCD THENA Auto)
      THEN Unfold `guard` 0
      THEN (RWO "member-fpf-domain" 0 THENM Reduce 0 THENM RWO "member_filter" 0)
      THEN Auto)xxx }

---

Latex:

---

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

---

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

---

Home Index