nadd_le_nadd_iff_right

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#Ordinal.nadd_le_nadd_iff_right

English

For all a, b, c, b ♯ a ≤ c ♯ a iff b ≤ c.

Русский

Для всех a, b, c верно: b ♯ a ≤ c ♯ a эквивалентно b ≤ c.

LaTeX

$$$$ b \# a \le c \# a \iff b \le c $$$$

Lean4

@[simp]
theorem nadd_le_nadd_iff_right : ∀ (a) {b c}, b ♯ a ≤ c ♯ a ↔ b ≤ c :=
  @_root_.add_le_add_iff_right NatOrdinal _ _ _ _

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

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

Разделы

Аффилиация

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