mrange_comp — Mathlib

English

For f : N →* O and g : M →* N, the range of the composition equals the image of the range of g under f: mrange(f.comp g) = (mrange g).map f.

Русский

Для моноидных гомоморфизмов f : N →* O и g : M →* N: mrange(f ∘ g) = (mrange g).map f.

LaTeX

$$$$ \\mathrm{mrange}(f \\circ g) = (\\mathrm{mrange}\;g).\\mathrm{map}\;f $$$$

Lean4

@[to_additive]
theorem mrange_comp {O : Type*} [MulOneClass O] (f : N →* O) (g : M →* N) : mrange (f.comp g) = (mrange g).map f :=
  SetLike.coe_injective <| Set.range_comp f _

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