add_eq_right_iff

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

Let a and b be cardinals. Then a + b = b if and only if either a = 0 or b ≥ max(aleph0, a).

Русский

Пусть a и b — кардиналы. Тогда a + b = b эквивалентно либо a = 0, либо b ≥ max(ℵ0, a).

LaTeX

$$$a + b = b \iff \max(\aleph_0, a) \le b \ \lor\ a = 0$$$

Lean4

theorem add_eq_right_iff {a b : Cardinal} : a + b = b ↔ max ℵ₀ a ≤ b ∨ a = 0 := by rw [add_comm, add_eq_left_iff]

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

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

Разделы

Аффилиация

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