range_comp_le_range — Mathlib

English

The carrier of the restricted range equals the image of the underlying function: ((NonUnitalAlgHom.range φ) : Set B) = Set.range (φ : A → B).

Русский

Носитель ограниченного образа совпадает с множеством изображений: носитель образа φ равен множеству {φ(a) | a ∈ A}.

LaTeX

$$$((\\mathrm{NonUnitalAlgHom.range}\\, φ) : \\mathrm{Set}\\ B) = \\{ φ(a) : a \\in A \\}$$$

Lean4

theorem range_comp_le_range (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) :
    NonUnitalAlgHom.range (g.comp f) ≤ NonUnitalAlgHom.range g :=
  SetLike.coe_mono (Set.range_comp_subset_range f g)

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