mrange_eq_iSup — Mathlib

English

The supremum over i of the ranges of the injections of M_i into CoprodI M equals the whole CoprodI; i.e., the images generate the coproduct.

Русский

Наименьшее верхнее число по i для образов внедрений M_i в CoprodI M даёт весь CoprodI; образы порождают копродукт.

LaTeX

$$$\\bigl(\\bigcup_i \\mathrm{mrange}(\\mathrm{of}_i)\\bigr) = \\top.$$$

Lean4

theorem mrange_eq_iSup {N} [Monoid N] (f : ∀ i, M i →* N) : MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i) :=
  by
  rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift, range_sigma_eq_iUnion_range,
    Submonoid.closure_iUnion]
  simp only [MonoidHom.mclosure_range]

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