lowerPolar_iUnion₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lowerPolar_iUnion₂ (f : ∀ i, κ i → Set β) : lowerPolar r (⋃ (i) (j), f i j) = ⋂ (i) (j), lowerPolar r (f i j) :=
  upperPolar_iUnion₂ ..

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