closure_range_inl_union_inr — Mathlib

English

The subgroup generated by the ranges of the two canonical injections inl: G → G ∗ H and inr: H → G ∗ H is the whole coproduct.

Русский

Подгруппа, порождённая образами двух канонических вложений inl: G → G ∗ H и inr: H → G ∗ H, равна всему копродукту.

LaTeX

$$$\operatorname{clo sure}\big(\mathrm{range}(\mathrm{inl}) \cup \mathrm{range}(\mathrm{inr})\big) = \top.$$$

Lean4

@[to_additive (attr := simp)]
theorem closure_range_inl_union_inr : Subgroup.closure (range (inl : G →* G ∗ H) ∪ range inr) = ⊤ :=
  Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_range_inl_union_inr

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