lowerClosure_iUnion — Mathlib

English

The lower closure distributes over indexed unions: lowerClosure (⋃ i, f(i)) = ⨆ i, lowerClosure (f(i)).

Русский

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

LaTeX

$$$\mathrm{lowerClosure}\Bigl(\bigcup_i f(i)\Bigr) = \bigvee_i \mathrm{lowerClosure}(f(i))$$$

Lean4

@[simp]
theorem lowerClosure_iUnion (f : ι → Set α) : lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i) :=
  (@gc_lowerClosure_coe α _).l_iSup

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