Step
*
of Lemma
fpf-restrict-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[f:x:A fp-> B[x]]. ∀[P:A ─→ 𝔹]. ∀[x:A].
uiff(↑x ∈ dom(fpf-restrict(f;P));{(↑x ∈ dom(f)) ∧ (↑(P x))})
BY
{ (UniformUnivCD Auto THEN Try (RemoveUiff) THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1))) }
1
∀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))})
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].
uiff(\muparrow{}x \mmember{} dom(fpf-restrict(f;P));\{(\muparrow{}x \mmember{} dom(f)) \mwedge{} (\muparrow{}(P x))\})
By
(UniformUnivCD Auto THEN Try (RemoveUiff) THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1)))
Home
Index