rangeRestrict — Mathlib

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)

Похожие утверждения