iSup_mrange_of — Mathlib

English

The supremum over i of the ranges of the injections of M_i into CoprodI M is the top submonoid; equivalently, every element of CoprodI M lies in the range of some of the injections.

Русский

Супремум по i образов внедрений M_i в CoprodI M равен верхнему подмоноиду; эквивалентно, любой элемент CoprodI M лежит в образе некоторого внедрения.

LaTeX

$$$\\bigl( \\bigsqcup_i \\mathrm{mrange}(\\mathrm{of}: M_i \\to CoprodI M) \\bigr) = \\top$$$

Lean4

@[simp]
theorem iSup_mrange_of : ⨆ i, MonoidHom.mrange (of : M i →* CoprodI M) = ⊤ := by simp [← mrange_eq_iSup]

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