iSup_eq_closure — Mathlib

English

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

Русский

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

LaTeX

$$$$ \big\vee_i S_i = \operatorname{closure}_L\left( \bigcup_i (S_i : \text{Set} M) \right). $$$$

Lean4

theorem iSup_eq_closure {ι : Sort*} (S : ι → L.Substructure M) : ⨆ i, S i = closure L (⋃ i, (S i : Set M)) := by
  simp_rw [closure_iUnion, closure_eq]
    -- This proof uses the fact that `Substructure.closure` is finitary.

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