mul_eq_max_of_aleph0_le_left — Mathlib

English

If a ≥ ℵ₀ and b ≠ 0, then a · b = max(a, b).

Русский

Если a ≥ ℵ₀ и b ≠ 0, то a · b = max(a, b).

LaTeX

$$$$(\aleph_0 \le a) \land (b \neq 0) \Rightarrow a \cdot b = \max(a,b)$$$$

Lean4

theorem mul_eq_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) (h' : b ≠ 0) : a * b = max a b :=
  by
  rcases le_or_gt ℵ₀ b with hb | hb
  · exact mul_eq_max h hb
  refine (mul_le_max_of_aleph0_le_left h).antisymm ?_
  have : b ≤ a := hb.le.trans h
  rw [max_eq_left this]
  convert mul_le_mul_left' (one_le_iff_ne_zero.mpr h') a
  rw [mul_one]

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