infinite_mul — Mathlib

English

The set product s * t is infinite exactly when either s is infinite and t is nonempty, or t is infinite and s is nonempty.

Русский

Произведение множеств s * t бесконечно тогда, когда либо s бесконечно и t непусто, либо t бесконечно и s непусто.

LaTeX

$$$$ (s * t).Infinite \\leftrightarrow s.Infinite \\land t.Nonempty \\lor t.Infinite \\land s.Nonempty $$$$

Lean4

@[to_additive]
theorem infinite_mul : (s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty :=
  infinite_image2 (fun _ _ => (mul_left_injective _).injOn) fun _ _ => (mul_right_injective _).injOn

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