mul_eq_max'

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.mul_eq_max'

← MathLib Explorer

English

If ℵ₀ ≤ a · b, then a · b = max(a, b).

Русский

Если ℵ₀ ≤ a · b, тогда a · b = max(a, b).

LaTeX

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

Lean4

theorem mul_eq_max' {a b : Cardinal} (h : ℵ₀ ≤ a * b) : a * b = max a b :=
  by
  rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩
  · exact mul_eq_max_of_aleph0_le_left ha' hb
  · exact mul_eq_max_of_aleph0_le_right ha hb'

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru