add_le_max — Mathlib

English

If ℵ₀ ≤ a and b ≤ a and b ≠ 0, then a · b = a.

Русский

Если ℵ₀ ≤ a, b ≤ a и b ≠ 0, то a · b = a.

LaTeX

$$$${(\aleph_0 \le a)} \land (b \le a) \land (b \neq 0) \Rightarrow a \cdot b = a$$$$

Lean4

theorem add_le_max (a b : Cardinal) : a + b ≤ max (max a b) ℵ₀ :=
  by
  rcases le_or_gt ℵ₀ a with ha | ha
  · rw [add_eq_max ha]
    exact le_max_left _ _
  · rcases le_or_gt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

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