one_pos'

Mathlib.Data.Fin.SuccPred

URI: https://scilib.ai/kg/mathlib#Fin.one_pos'

English

In Fin(n+1), 0 < 1 holds when NeZero n.

Русский

В Fin(n+1) выполняется 0 < 1 при NeZero n.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ [\\mathrm{NeZero}\\ n] : (0: \\mathrm{Fin}(n+1)) < 1$$$

Lean4

theorem one_pos' [NeZero n] : (0 : Fin (n + 1)) < 1 :=
  succ_zero_eq_one' (n := n) ▸ succ_pos _

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

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

Разделы

Аффилиация

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