sUnion — Mathlib

English

If a set s of sets is infinite, then the union ⋃ s is infinite.

Русский

Если множество s состоит из бесконечного числа подмножеств, то объединение ⋃ s бесконечно.

LaTeX

$$$s \text{ infinite} \Rightarrow (\bigcup s) \text{ is Infinite}$$$

Lean4

theorem sUnion {s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite :=
  by
  rw [sUnion_eq_iUnion]
  have _ := hs.to_subtype
  exact infinite_iUnion Subtype.coe_injective

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