Restriction

• Restriction #Card
  • For $V \subset X$, $f|_V : V \to Y$ is defined by $f|_V(x) := f(x)$ for $x \in V$.

Back

For $V \subset X$, $f|_V : V \to Y$ is defined by $f|_V(x) := f(x)$ for $x \in V$.

Lean

Set.restrict / Function.restrict (f ∘ Subtype.val)