val_comp_codRestrict — Mathlib

English

The underlying function value of the codomain-restricted map agrees with f on every input.

Русский

Пусть f ограничен в кодом S; его базовая функция на входе x совпадает с f(x).

LaTeX

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

Lean4

@[simp]
theorem val_comp_codRestrict (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ x, f x ∈ S) :
    S.val.comp (f.codRestrict S hf) = f :=
  AlgHom.ext fun _ => rfl

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