infinite_iUnion — Mathlib

English

Let ι be an infinite index set and s : ι → Set α be injective. Then the union ⋃_{i} s(i) is infinite.

Русский

Пусть ι бесконечно, и функция s : ι → множество α задаёт попарно различные подмножества. Тогда объединение ⋃_{i} s(i) бесконечно.

LaTeX

$$$\text{If } ι \text{ is infinite and } s: ι \to \mathcal P(α) \text{ is injective, then } (\bigcup_{i} s(i)) \text{ is Infinite}.$$$

Lean4

theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) : (⋃ i, s i).Infinite :=
  fun hfin ↦
  @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦
    hs (by simpa using h_eq)

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