isUpperSet_iUnion₂ — Mathlib

English

If f(i) is upper for each i and j, then the two-parameter union is upper: ⋃ i ⋃ j f(i,j) is upper.

Русский

Если f(i,j) верхнее для всех i и j, то двойное объединение верхнее: ⋃ i ⋃ j f(i,j) — верхнее множество.

LaTeX

$$$\forall i, \forall j, IsUpperSet(f(i, j)) \Rightarrow IsUpperSet(\bigcup_i \bigcup_j f(i, j))$$$

Lean4

theorem isUpperSet_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsUpperSet (f i j)) : IsUpperSet (⋃ (i) (j), f i j) :=
  isUpperSet_iUnion fun i => isUpperSet_iUnion <| hf i

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