iSup_eq_closure — Mathlib

English

The supremum of a family of subgroups equals the closure of the union of their underlying sets.

Русский

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

LaTeX

$$$ \bigvee_{i} p(i) = \mathrm{closure}\left( \bigcup_{i} (p(i) : \mathrm{Set} \;G) \right) $$$

Lean4

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

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