English
The equality a + b = a holds iff max(ℵ₀, b) ≤ a or b = 0.
Русский
Равенство a + b = a выполняется тогда и только тогда, когда max(ℵ₀, b) ≤ a или b = 0.
LaTeX
$$$$ a + b = a \iff (\max(\aleph_0, b) \le a \lor b = 0) $$$$
Lean4
theorem add_eq_left_iff {a b : Cardinal} : a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0 :=
by
rw [max_le_iff]
refine ⟨fun h => ?_, ?_⟩
· rcases le_or_gt ℵ₀ a with ha | ha
· left
use ha
rw [← not_lt]
apply fun hb => ne_of_gt _ h
intro hb
exact hb.trans_le (self_le_add_left b a)
right
rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
norm_cast at h ⊢
rw [← add_right_inj, h, add_zero]
· rintro (⟨h1, h2⟩ | h3)
· rw [add_eq_max h1, max_eq_left h2]
· rw [h3, add_zero]
