lt_add_iff_pos_right

Mathlib.Data.Nat.PartENat

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

protected theorem lt_add_iff_pos_right {x y : PartENat} (hx : x ≠ ⊤) : x < x + y ↔ 0 < y :=
  by
  conv_rhs => rw [← PartENat.add_lt_add_iff_left hx]
  rw [add_zero]

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

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

Разделы

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

Аффилиация

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