range_comp — Mathlib

English

For L-homs f: M →[L] N and g: N →[L] P, the range of the composition equals the image of the range of f under g; i.e., range(g ∘ f) = map g (range f).

Русский

Для гомоморфизмов f: M →[L] N и g: N →[L] P образ композиции равен образу образа f под действием g: range(g∘f) = map g (range f).

LaTeX

$$$ \operatorname{range}(g\circ f) = \operatorname{map}~g(\operatorname{range}(f)) $$$

Lean4

theorem range_comp (f : M →[L] N) (g : N →[L] P) : range (g.comp f : M →[L] P) = map g (range f) :=
  SetLike.coe_injective (Set.range_comp g f)

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