iUnion — Mathlib

English

If s i j is Infinite for some i,j, then the double indexed union ⋃ i ⋃ j s i j is Infinite.

Русский

Если для каких-либо i,j множество s i j бесконечно, то двойное индексное объединение ⋃ i ⋃ j s i j бесконечно.

LaTeX

$$$\\operatorname{Infinite}\\left(\\bigcup_{i}\\bigcup_{j} s_{i j}\\right)$$$

Lean4

protected theorem iUnion {ι : Sort*} {s : ι → Set α} (i : ι) (hi : (s i).Infinite) : (⋃ i, s i).Infinite := fun h ↦
  hi (h.subset (Set.subset_iUnion s i))

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