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