upperClosure_sUnion — Mathlib

English

For any S ⊆ Set α, the upper closure of the sUnion over S equals the infimum over s ∈ S of upperClosure(s).

Русский

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

LaTeX

$$$\mathrm{upperClosure}(\bigcup_{S} S) = \bigwedge_{s\in S} \mathrm{upperClosure}(s)$$$

Lean4

@[simp]
theorem upperClosure_sUnion (S : Set (Set α)) : upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s := by
  simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]

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