mul_le_max_of_aleph0_le_right

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.mul_le_max_of_aleph0_le_right

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_le_max_of_aleph0_le_right {a b : Cardinal} (h : ℵ₀ ≤ b) : a * b ≤ max a b := by
  simpa only [mul_comm b, max_comm b] using mul_le_max_of_aleph0_le_left h

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

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

Разделы

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

Аффилиация

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