upperPolar_iUnion — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem upperPolar_iUnion (f : ι → Set α) : upperPolar r (⋃ i, f i) = ⋂ i, upperPolar r (f i) :=
  (gc_upperPolar_lowerPolar r).l_iSup

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