natCast_lt_succ

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.natCast_lt_succ

English

For every n ∈ ℕ, (n : ENat) < (n : ENat) + 1.

Русский

Для каждого n ∈ ℕ: (n: ENat) < (n: ENat) + 1.

LaTeX

$$$\forall {n : \mathbb{N}}, (n : \mathbb{N}_{\infty}) < (n : \mathbb{N}_{\infty}) + 1$$$

Lean4

theorem natCast_lt_succ {n : ℕ} : (n : ℕ∞) < (n : ℕ∞) + 1 :=
  by
  rw [← Nat.cast_one, ← Nat.cast_add, coe_lt_coe]
  exact lt_add_one n

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

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

Разделы

Аффилиация

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