coe_range — Mathlib

English

Composition of star-algebra homomorphisms respects range in a compatible way.

Русский

Состав гомоморфизмов сохраняет образ в согласованной форме.

LaTeX

$$NonUnitalStarAlgHom.range(g.comp f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)$$

Lean4

@[simp, norm_cast]
theorem coe_range (φ : F) :
    ((NonUnitalStarAlgHom.range φ : NonUnitalStarSubalgebra R B) : Set B) = Set.range (φ : A → B) := by ext;
  rw [SetLike.mem_coe, mem_range]; rfl

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