mul_le_max_of_aleph0_le_left — Mathlib

English

If a ≥ ℵ₀, then a · b ≤ max(a, b) for all cardinals b.

Русский

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

LaTeX

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

Lean4

theorem mul_le_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) : a * b ≤ max a b :=
  by
  convert mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
  rw [mul_eq_self]
  exact h.trans (le_max_left a b)

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