infinite_sum — Mathlib

English

For any α, β, the sum type α ⊕ β is infinite exactly when at least one of α or β is infinite.

Русский

Для любых α, β сумма α ⊕ β бесконечна тогда, когда хотя бы один из α или β бесконечен.

LaTeX

$$$$\\text{Infinite}(\\alpha \\oplus \\beta) \\iff \\text{Infinite}(\\alpha) \\lor \\text{Infinite}(\\beta).$$$$

Lean4

@[simp]
theorem infinite_sum : Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β :=
  by
  refine ⟨fun H => ?_, fun H => H.elim (@Sum.infinite_of_left α β) (@Sum.infinite_of_right α β)⟩
  contrapose! H; cases H
  infer_instance

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