English
For sets s, t, the product s × t is infinite if and only if either s is infinite and t is nonempty, or t is infinite and s is nonempty.
Русский
Для множеств S, T произведение S × T бесконечно тогда и только тогда, когда либо S бесконечно, и T непусто, либо T бесконечно, и S непусто.
LaTeX
$$$ |s \times t| = \infty \iff (|s| = \infty \land t \neq \emptyset) \lor (|t| = \infty \land s \neq \emptyset) $$$
Lean4
protected theorem infinite_prod : (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty :=
by
refine ⟨fun h => ?_, ?_⟩
· simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
by_contra!
exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)
· rintro (h | h)
· exact h.1.prod_left h.2
· exact h.1.prod_right h.2
