subtype_comp_codRestrict — Mathlib

English

The subtype-embedding composed with codRestrict equals the original map.

Русский

Образование подтипа композиции с codRestrict даёт исходную карту.

LaTeX

$$$((\\mathrm{Subtype}\\ S).comp (\\mathrm{codRestrict}\\ f\\ S\\ hf)) = f$$$

Lean4

@[simp]
theorem subtype_comp_codRestrict (f : F) (S : NonUnitalStarSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
    (NonUnitalStarSubalgebraClass.subtype S).comp (NonUnitalStarAlgHom.codRestrict f S hf) = f :=
  NonUnitalStarAlgHom.ext fun _ => rfl

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