lt_add_one

Mathlib.Data.Nat.PartENat

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

English

For any x ≠ ⊤, we have x < x + 1.

Русский

Для любого x ≠ ⊤ верно, что x < x+1.

LaTeX

$$$ \forall x: \mathrm{PartENat}, x \neq \top \Rightarrow x < x + 1$$$

Lean4

theorem lt_add_one {x : PartENat} (hx : x ≠ ⊤) : x < x + 1 :=
  by
  rw [PartENat.lt_add_iff_pos_right hx]
  norm_cast

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

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

Разделы

Аффилиация

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