isLowerSet_iUnion₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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