lowerPolar_iUnion — Mathlib

English

Lower polar commutes with indexed unions: lowerPolar r (⋃ i, f i) = ⋂ i, lowerPolar r (f i).

Русский

Lower polar коммутирует с инфиндексированными объединениями: lowerPolar r (⋃ i, f i) = ⋂ i, lowerPolar r (f i).

LaTeX

$$$\lowerPolar r (\bigcup_i f(i)) = \bigcap_i \lowerPolar r (f(i))$$$

Lean4

@[simp]
theorem lowerPolar_iUnion (f : ι → Set β) : lowerPolar r (⋃ i, f i) = ⋂ i, lowerPolar r (f i) :=
  upperPolar_iUnion ..

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