mrange_inl_sup_mrange_inr — Mathlib

English

The join of the ranges of inl and inr equals the whole coproduct in terms of MonoidHommrange.

Русский

Слияние образов inl и inr равно всему копродукту по образам мрэнджа.

LaTeX

$$$\operatorname{mrange}(\mathrm{inl}) \sqcup \operatorname{mrange}(\mathrm{inr}) = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem mrange_inl_sup_mrange_inr : MonoidHom.mrange (inl : M →* M ∗ N) ⊔ MonoidHom.mrange (inr : N →* M ∗ N) = ⊤ := by
  rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange, ← MonoidHom.coe_mrange,
    Submonoid.closure_eq, Submonoid.closure_eq]

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