mclosure_iUnion_range_of — Mathlib

English

Let (M_i) be a family of monoids indexed by ι and CoprodI M the coproduct monoid. The submonoid of CoprodI M generated by all copies of the M_i (via the canonical injections) is the whole CoprodI M.

Русский

Пусть (M_i) — семья моноидов, индексируемая ι, и CoprodI M — их копродукт. Подмоноид CoprodI M, порождённый изображениями всех факторов через канонические внедрения, равен всему CoprodI M.

LaTeX

$$$\operatorname{Submonoid}.closure\Big(\bigcup_{i} \operatorname{range} (\mathrm{of} : M_i \to_* \mathrm{CoprodI} M)\Big) = \top$$$

Lean4

@[simp]
theorem mclosure_iUnion_range_of : Submonoid.closure (⋃ i, Set.range (of : M i →* CoprodI M)) = ⊤ := by
  simp [Submonoid.closure_iUnion]

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