English
Infinite (α × β) is equivalent to Either Infinite α and Nonempty β or Nonempty α and Infinite β.
Русский
Бесконечность α×β эквивалентна либо бесконечности α и непустости β, либо непустости α и бесконечности β.
LaTeX
$$$\\text{Infinite}(\\alpha \\times \\beta) \\iff (\\text{Infinite}(\\alpha) \\land \\text{Nonempty}(\\beta)) \\lor (\\text{Nonempty}(\\alpha) \\land \\text{Infinite}(\\beta)).$$$
Lean4
@[simp]
theorem infinite_prod : Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β :=
by
refine
⟨fun H => ?_, fun H => H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
rw [and_comm]
rcases Infinite.nonempty (α × β) with ⟨a, b⟩
contrapose! H; haveI := H.1 ⟨b⟩; haveI := H.2 ⟨a⟩
infer_instance
