infinite_union — Mathlib

English

The union of two sets is infinite iff at least one of them is infinite.

Русский

Объединение двух множеств бесконечно тогда и только тогда, когда хотя бы одно из множеств бесконечно.

LaTeX

$$$ (s \cup t) \text{ Infinite} \iff s.\text{Infinite} \lor t.\text{Infinite} $$$

Lean4

@[simp]
theorem infinite_union {s t : Set α} : (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite := by
  simp only [Set.Infinite, finite_union, not_and_or]

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