English
The coercion of codRestrict respects evaluation on input x, i.e., the value equals f(x).
Русский
Приведение к codRestrict сохраняет вычисление на входе x: равняется f(x).
LaTeX
$$$\\uparrow(\\text{codRestrict } f S hf \\, x) = f(x)$$$
Lean4
/-- Restrict the codomain of an `NonUnitalAlgHom` `f` to `f.range`.
This is the bundled version of `Set.rangeFactorization`. -/
abbrev rangeRestrict (f : F) : A →ₙₐ[R] (NonUnitalAlgHom.range f : NonUnitalSubalgebra R B) :=
NonUnitalAlgHom.codRestrict f (NonUnitalAlgHom.range f) (NonUnitalAlgHom.mem_range_self f)