sup_eq_closure — Mathlib

English

For submonoids N and N' of M, their supremum equals the closure of their underlying sets: N ⊔ N' = closure((N : Set M) ∪ (N' : Set M)).

Русский

Для подмоноидов N и N' в M их наибольшая верхняя граница равна замыканию от объединения соответствующих множеств: N ⊔ N' = closure((N : Set M) ∪ (N' : Set M)).

LaTeX

$$$N \\sqcup N' = \\operatorname{closure}((N : \\mathrm{Set} M) \\cup (N' : \\mathrm{Set} M))$$$

Lean4

@[to_additive]
theorem sup_eq_closure (N N' : Submonoid M) : N ⊔ N' = closure ((N : Set M) ∪ (N' : Set M)) := by
  simp_rw [closure_union, closure_eq]

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