sup_eq_range — Mathlib

English

In a commutative monoid N, the supremum (join) of two submonoids s and t equals the image under the coprod map of their subtypes; i.e., s ⊔ t = mrange (s.subtype.coprod t.subtype).

Русский

В коммутативном моноиде N сумма (объединение) двух подмоноидов s и t равна образу через coprod-произведение их подтипов; т.е. s ⊔ t = mrange (s.subtype.coprod t.subtype).

LaTeX

$$$ s \\sqcup t = \\mathrm{mrange}(s.subtype.coprod t.subtype) $$$

Lean4

@[to_additive]
theorem sup_eq_range (s t : Submonoid N) : s ⊔ t = mrange (s.subtype.coprod t.subtype) := by
  rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange, coprod_comp_inr,
    mrange_subtype, mrange_subtype]

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