coe_codRestrict

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#AlgHom.coe_codRestrict

English

Same as above: the value of the codomain-restricted map at x equals f(x).

Русский

То же самое: значение ограниченного по коду отображения в точке x равно f(x).

LaTeX

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

Lean4

@[simp]
theorem coe_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) (x : A) :
    ↑(f.codRestrict S hf x) = f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru