range_eq — Mathlib

English

For any f: G ∗ H → K, the range of f equals the supremum of the ranges of f ∘ inl and f ∘ inr.

Русский

Для любого отображения f: G ∗ H → K образ f равен верхней границе образов f ∘ inl и f ∘ inr.

LaTeX

$$$\mathrm{range}(f) = \mathrm{range}(f\circ inl) \lor \mathrm{range}(f\circ inr).$$$

Lean4

@[to_additive]
theorem range_eq (f : G ∗ H →* K) : MonoidHom.range f = MonoidHom.range (f.comp inl) ⊔ MonoidHom.range (f.comp inr) :=
  by rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range, MonoidHom.map_range]

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