mrange_eq — Mathlib

English

For any f: M ∗ N →* P, the image of f equals the join of the images of f∘inl and f∘inr.

Русский

Для любого отображения f: M ∗ N →* P образ f равен объединению образов f ∘ inl и f ∘ inr.

LaTeX

$$$\operatorname{MonoidHom.mrange}(f) = \operatorname{mrange}(f\circ \mathrm{inl}) \sqcup \operatorname{mrange}(f\circ \mathrm{inr}).$$$

Lean4

@[to_additive]
theorem mrange_eq (f : M ∗ N →* P) :
    MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr) := by
  rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]

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