upperClosure_iUnion — Mathlib

English

The upper closure distributes over indexed unions: upperClosure (⋃ i, f(i)) = ⨅ i, upperClosure(f(i)).

Русский

Верхнее замыкание распределяется по индексированным объединениям: верхнее замыкание ⋃i f(i) = ⋂i верхнее замыкание f(i).

LaTeX

$$$\mathrm{upperClosure}\Bigl(\bigcup_i f(i)\Bigr) = \bigwedge_i \mathrm{upperClosure}(f(i))$$$

Lean4

@[simp]
theorem upperClosure_iUnion (f : ι → Set α) : upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i) :=
  (@gc_upperClosure_coe α _).l_iSup

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