coe_codRestrict — Mathlib

English

Restricting to a subalgebra and composing with codRestrict yields the original f.

Русский

Ограничение к подалгебре и компоновка с codRestrict восстанавливают исходное отображение.

LaTeX

$$(subtype S).comp (codRestrict f S hf) = f$$

Lean4

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

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