add_eq_right

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

If ℵ₀ ≤ b and a ≤ b, then a + b = b.

Русский

Если ℵ₀ ≤ b и a ≤ b, то a + b = b.

LaTeX

$$$$(\aleph_0 \le b) \land (a \le b) \Rightarrow a + b = b$$$$

Lean4

theorem add_eq_right {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) : a + b = b := by rw [add_comm, add_eq_left hb ha]

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

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

Разделы

Аффилиация

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