mul_eq_left

Mathlib.SetTheory.Cardinal.Arithmetic

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

← MathLib Explorer

English

If a ≥ ℵ₀ and b ≤ a and b ≠ 0, then a · b = a.

Русский

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

LaTeX

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

Lean4

theorem mul_eq_left {a b : Cardinal} (ha : ℵ₀ ≤ a) (hb : b ≤ a) (hb' : b ≠ 0) : a * b = a := by
  rw [mul_eq_max_of_aleph0_le_left ha hb', max_eq_left hb]

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

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

Разделы

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

Аффилиация

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