sup — Mathlib

English

The supremum of two finitely generated subgroups is finitely generated.

Русский

Супремум двух конечнопорожденных подгрупп порожден конечным числом элементов.

LaTeX

$$$\forall P Q : Subgroup G, P.FG \to Q.FG \to (P \sqcup Q).FG$$$

Lean4

@[to_additive]
theorem sup {P Q : Subgroup G} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG := by
  classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩

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