upperPolar_iUnion₂ — Mathlib

English

Upper polar distributes over double indexed unions: upperPolar r (⋃ i (⋃ j, f(i,j))) = ⋂ i (⋂ j, upperPolar r (f(i,j))).

Русский

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

LaTeX

$$$\upperPolar r (\cup_i \cup_j f(i,j)) = \bigcap_i \bigcap_j \upperPolar r (f(i,j))$$$

Lean4

theorem upperPolar_iUnion₂ (f : ∀ i, κ i → Set α) : upperPolar r (⋃ (i) (j), f i j) = ⋂ (i) (j), upperPolar r (f i j) :=
  (gc_upperPolar_lowerPolar r).l_iSup₂

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