iSup_eq_closure — Mathlib

English

The supremum of a family of subsemigroups equals the closure of the union of their carriers.

Русский

Наибольший элемент семейства подполугрупп равен замыканию объединения их множеств.

LaTeX

$$$\\bigvee_{i} p_i = \\mathrm{closure}\\left( \\bigcup_{i} (p_i : Set M) \\right)$$$

Lean4

@[to_additive]
theorem iSup_eq_closure {ι : Sort*} (p : ι → Subsemigroup M) : ⨆ i, p i = Subsemigroup.closure (⋃ i, (p i : Set M)) :=
  by simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

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