add_one_le_add_one_iff

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For cardinals α,β, α + 1 ≤ β + 1 iff α ≤ β.

Русский

Для кардиналов α,β: α + 1 ≤ β + 1 эквивалентно α ≤ β.

LaTeX

$$$α + 1 ≤ β + 1 \iff α ≤ β$$$

Lean4

@[simp]
theorem add_one_le_add_one_iff {α β : Cardinal} : α + 1 ≤ β + 1 ↔ α ≤ β :=
  add_le_add_iff_of_lt_aleph0 one_lt_aleph0

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

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

Разделы

Аффилиация

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