mul_le_max — Mathlib

English

For any cardinals a and b, a · b ≤ max(max(a, b), ℵ₀).

Русский

Для любых кардиналов a и b справедливо a · b ≤ max(max(a, b), ℵ₀).

LaTeX

$$$$(a,b : Cardinal) \Rightarrow a \cdot b \le \max(\max(a,b), \aleph_0)$$$$

Lean4

theorem mul_le_max (a b : Cardinal) : a * b ≤ max (max a b) ℵ₀ :=
  by
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rcases eq_or_ne b 0 with (rfl | hb0); · simp
  rcases le_or_gt ℵ₀ a with ha | ha
  · rw [mul_eq_max_of_aleph0_le_left ha hb0]
    exact le_max_left _ _
  · rcases le_or_gt ℵ₀ b with hb | hb
    · rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

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