English
For any a,b, a · b < aleph0 iff a = 0 or b = 0 or both a,b < aleph0.
Русский
Для любых a,b: a · b < aleph0 тогда и только тогда a = 0 или b = 0 или оба a,b < aleph0.
LaTeX
$$$ a \cdot b < \aleph_0 \iff a = 0 \lor b = 0 \lor (a < \aleph_0 \land b < \aleph_0) $$$
Lean4
theorem mul_lt_aleph0_iff {a b : Cardinal} : a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ :=
by
refine ⟨fun h => ?_, ?_⟩
· by_cases ha : a = 0
· exact Or.inl ha
right
by_cases hb : b = 0
· exact Or.inl hb
right
rw [← Ne, ← one_le_iff_ne_zero] at ha hb
constructor
· rw [← mul_one a]
exact (mul_le_mul' le_rfl hb).trans_lt h
· rw [← one_mul b]
exact (mul_le_mul' ha le_rfl).trans_lt h
rintro (rfl | rfl | ⟨ha, hb⟩) <;> simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]
