eq_of_add_eq_add_right

Mathlib.SetTheory.Cardinal.Arithmetic

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

← MathLib Explorer

English

For cardinals a,b,c with b < aleph0, if a + b = c + b then a = c.

Русский

Для кардиналов a,b,c, если b < ℵ0 и a + b = c + b, то a = c.

LaTeX

$$$(a + b = c + b) \land (b < \aleph_0) \Rightarrow a = c$$$

Lean4

protected theorem eq_of_add_eq_add_right {a b c : Cardinal} (h : a + b = c + b) (hb : b < ℵ₀) : a = c :=
  by
  rw [add_comm a b, add_comm c b] at h
  exact Cardinal.eq_of_add_eq_add_left h hb

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

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

Разделы

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

Аффилиация

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