range_inl_sup_range_inr — Mathlib

English

The join (supremum) of the ranges of inl and inr equals the whole group.

Русский

Объединение образов inl и inr образует всю группу.

LaTeX

$$$ \mathrm{range}(\mathrm{inl}) \sqcup \mathrm{range}(\mathrm{inr}) = \top. $$$

Lean4

@[to_additive (attr := simp)]
theorem range_inl_sup_range_inr : MonoidHom.range (inl : G →* G ∗ H) ⊔ MonoidHom.range inr = ⊤ := by
  rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range, ← MonoidHom.coe_range,
    Subgroup.closure_eq, Subgroup.closure_eq]

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