add_lt_add_iff_left

Mathlib.Data.Nat.PartENat

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

← MathLib Explorer

English

For z ≠ ⊤, z + x < z + y iff x < y.

Русский

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

LaTeX

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

Lean4

protected theorem add_lt_add_iff_left {x y z : PartENat} (hz : z ≠ ⊤) : z + x < z + y ↔ x < y := by
  rw [add_comm z, add_comm z, PartENat.add_lt_add_iff_right hz]

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

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

Разделы

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

Аффилиация

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