natCast_mono

Mathlib.Data.Fin.Basic

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

English

If b ≤ n and a ≤ b then (a : Fin (n+1)) ≤ b.

Русский

Если b ≤ n и a ≤ b, то (a : Fin (n+1)) ≤ b.

LaTeX

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

Lean4

theorem natCast_mono (hbn : b ≤ n) (hab : a ≤ b) : (a : Fin (n + 1)) ≤ b :=
  (natCast_le_natCast (hab.trans hbn) hbn).2 hab

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

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

Разделы

Аффилиация

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