add_eq_max — Mathlib

English

For all a,b, if ℵ₀ ≤ a, then a + b = max(a,b).

Русский

Для всех a,b при ℵ₀ ≤ a верно a + b = max(a,b).

LaTeX

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

Lean4

/-- If `α` is an infinite type, then the cardinality of `α ⊕ β` is the maximum
of the cardinalities of `α` and `β`. -/
theorem add_eq_max {a b : Cardinal} (ha : ℵ₀ ≤ a) : a + b = max a b :=
  le_antisymm (add_eq_self (ha.trans (le_max_left a b)) ▸ add_le_add (le_max_left _ _) (le_max_right _ _)) <|
    max_le (self_le_add_right _ _) (self_le_add_left _ _)

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