iSup_eq_closure — Mathlib

English

The supremum of a family of submonoids equals the closure of the union of their underlying sets: ⨆ i, p_i = closure(⋃ i, (p_i : Set M)).

Русский

Наибольшая верхняя граница семейства подмономов равна замыканию объединения их множества: ⨆ i, p_i = closure(⋃ i, (p_i : Set M)).

LaTeX

$$$\\bigvee_i p_i = \\operatorname{closure}\\big(\\bigcup_i (p_i : \\mathrm{Set} M)\\big)$$$

Lean4

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

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