natCast_strictMono

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.natCast_strictMono

English

If n is finite and b ≤ n and a < b, then (a : Fin (n+1)) < b.

Русский

Если n конечно и b ≤ n, a < b, то (a : Fin (n+1)) < b.

LaTeX

$$$\\forall {n,a,b} \\in \\mathbb{N}, \\; b \\le n \\to a < b \\to (a : \\mathrm{Fin}(n+1)) < b$$$

Lean4

theorem natCast_strictMono (hbn : b ≤ n) (hab : a < b) : (a : Fin (n + 1)) < b :=
  (natCast_lt_natCast (hab.le.trans hbn) hbn).2 hab

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

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

Разделы

Аффилиация

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