add_lt_add_iff_right

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.add_lt_add_iff_right

← MathLib Explorer

English

For z ≠ ⊤, x + z < y + z if and only if x < y.

Русский

Для z ≠ ⊤, x+z < y+z тогда и только тогда, когда x < y.

LaTeX

$$$ \forall x,y,z: \mathrm{PartENat}, z \neq \top \Rightarrow (x+z < y+z) \iff (x < y)$$$

Lean4

protected theorem add_lt_add_iff_right {x y z : PartENat} (hz : z ≠ ⊤) : x + z < y + z ↔ x < y :=
  ⟨lt_of_add_lt_add_right, fun h => PartENat.add_lt_add_right h hz⟩

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

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

Разделы

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

Аффилиация

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