English
For cardinals a,b,c with a < aleph0, from a + b = a + c one deduces b = c.
Русский
Для кардиналов a,b,c, где a < ℵ0, из a + b = a + c следует b = c.
LaTeX
$$$a < \aleph_0 \Rightarrow (a + b = a + c) \Rightarrow b = c$$$
Lean4
protected theorem eq_of_add_eq_add_left {a b c : Cardinal} (h : a + b = a + c) (ha : a < ℵ₀) : b = c :=
by
rcases le_or_gt ℵ₀ b with hb | hb
· have : a < b := ha.trans_le hb
rw [add_eq_right hb this.le, eq_comm] at h
rw [eq_of_add_eq_of_aleph0_le h this hb]
· have hc : c < ℵ₀ := by
rw [← not_le]
intro hc
apply lt_irrefl ℵ₀
apply (hc.trans (self_le_add_left _ a)).trans_lt
rw [← h]
apply add_lt_aleph0 ha hb
rw [lt_aleph0] at *
rcases ha with ⟨n, rfl⟩
rcases hb with ⟨m, rfl⟩
rcases hc with ⟨k, rfl⟩
norm_cast at h ⊢
apply add_left_cancel h
