lowerClosure_sUnion — Mathlib

English

For any S ⊆ Set α, the lower closure of the sUnion over S equals the supremum over s ∈ S of lowerClosure(s).

Русский

Для любого S ⊆ Set α нижнее замыкание объединения S равно объединению нижних замыканий элементов S.

LaTeX

$$$\mathrm{lowerClosure}(\bigcup_{S} S) = \bigvee_{s\in S} \mathrm{lowerClosure}(s)$$$

Lean4

@[simp]
theorem lowerClosure_sUnion (S : Set (Set α)) : lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s := by
  simp_rw [sUnion_eq_biUnion, lowerClosure_iUnion]

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