mclosure_range_inl_union_inr — Mathlib

English

The submonoid generated by the ranges of inl and inr equals the entire coproduct Monoid.Coprod M N.

Русский

Левая и правая вложения порождают весь копродукт.

LaTeX

$$$\operatorname{Submonoid.closure}(\operatorname{range}(\mathrm{inl}) \cup \operatorname{range}(\mathrm{inr})) = \top$.$$

Lean4

@[to_additive (attr := simp)]
theorem mclosure_range_inl_union_inr : Submonoid.closure (range (inl : M →* M ∗ N) ∪ range (inr : N →* M ∗ N)) = ⊤ := by
  rw [← mrange_mk, MonoidHom.mrange_eq_map, ← closure_range_of, MonoidHom.map_mclosure, ← range_comp, Sum.range_eq]; rfl

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