lt_succ_self

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.lt_succ_self

English

For any a ∈ ℕ⁺, a < succPNat a.

Русский

Для любого a ∈ ℕ⁺ выполняется a < succPNat a.

LaTeX

$$$$ \forall a \in \mathbb{N}_{>0},\; a < \text{succPNat}(a) $$$$

Lean4

theorem lt_succ_self (a : ℕ+) : a < succPNat a :=
  lt.base a

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

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

Разделы

Аффилиация

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