add_eq_self — Mathlib

English

If ℵ₀ ≤ a, then a + b = max(a, b) for all b.

Русский

Если ℵ₀ ≤ a, то a + b = max(a, b) для любого b.

LaTeX

$$$$(\aleph_0 \le a) \Rightarrow a + b = \max(a,b)$$$$

Lean4

/-- If `α` is an infinite type, then `α ⊕ α` and `α` have the same cardinality. -/
theorem add_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c + c = c :=
  le_antisymm (by convert mul_le_mul_right' ((nat_lt_aleph0 2).le.trans h) c using 1 <;> simp [two_mul, mul_eq_self h])
    (self_le_add_left c c)

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