add_nat_le_add_nat_iff

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For n ∈ ℕ, α + n ≤ β + n iff α ≤ β.

Русский

Для n ∈ ℕ: α + n ≤ β + n эквивалентно α ≤ β.

LaTeX

$$$n \in \mathbb{N} \Rightarrow (\alpha + n \le \beta + n) \iff (\alpha \le \beta)$$$

Lean4

@[simp]
theorem add_nat_le_add_nat_iff {α β : Cardinal} (n : ℕ) : α + n ≤ β + n ↔ α ≤ β :=
  add_le_add_iff_of_lt_aleph0 (nat_lt_aleph0 n)

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

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

Разделы

Аффилиация

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