rangeRestrict — Mathlib

English

Same as 1338: the value of the restricted map equals the original on inputs.

Русский

Как и в 1338: значение ограниченного отображения равно исходному на входах.

LaTeX

$$$ \uparrow\bigl(f.\mathrm{codRestrict} S hf\; x\bigr) = f(x)$$$

Lean4

/-- Restrict the codomain of an `AlgHom` `f` to `f.range`.

This is the bundled version of `Set.rangeFactorization`. -/
abbrev rangeRestrict (f : A →ₐ[R] B) : A →ₐ[R] f.range :=
  f.codRestrict f.range f.mem_range_self

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