eq_of_add_eq_of_aleph0_le — Mathlib

English

If a + b = c with a < c and ℵ₀ ≤ c, then b = c.

Русский

Если a + b = c, при этом a < c и ℵ₀ ≤ c, то b = c.

LaTeX

$$$$ (a + b = c) \land (a < c) \land (\aleph_0 \le c) \Rightarrow b = c$$$$

Lean4

theorem eq_of_add_eq_of_aleph0_le {a b c : Cardinal} (h : a + b = c) (ha : a < c) (hc : ℵ₀ ≤ c) : b = c :=
  by
  apply le_antisymm
  · rw [← h]
    apply self_le_add_left
  rw [← not_lt]; intro hb
  have : a + b < c := add_lt_of_lt hc ha hb
  simp [h] at this

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