cast_add_one_pos

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#Nat.cast_add_one_pos

English

For every n ∈ ℕ, the sum (n : α) + 1 is strictly positive: 0 < (n : α) + 1.

Русский

Для каждого n ∈ ℕ сумма (n : α) + 1 строго положительна: 0 < (n : α) + 1.

LaTeX

$$$\forall n \in \mathbb{N},\ 0 < (n : \alpha) + 1.$$$

Lean4

theorem cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1 :=
  by
  apply zero_lt_one.trans_le
  convert (@mono_cast α _).imp (?_ : 1 ≤ n + 1) <;> simp

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

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

Разделы

Аффилиация

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