mul_eq_max — Mathlib

English

For infinite cardinals a,b, a × b = max(a,b) provided a,b ≥ ℵ0.

Русский

Для бесконечных кардиналов a,b выполняется a × b = max(a,b), если a,b ≥ ℵ0.

LaTeX

$$$a \times b = \max\{a,b\}$$$

Lean4

/-- If `α` and `β` are infinite types, then the cardinality of `α × β` is the maximum
of the cardinalities of `α` and `β`. -/
theorem mul_eq_max {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : ℵ₀ ≤ b) : a * b = max a b :=
  le_antisymm (mul_eq_self (ha.trans (le_max_left a b)) ▸ mul_le_mul' (le_max_left _ _) (le_max_right _ _)) <|
    max_le (by simpa only [mul_one] using mul_le_mul_left' (one_le_aleph0.trans hb) a)
      (by simpa only [one_mul] using mul_le_mul_right' (one_le_aleph0.trans ha) b)

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