sub_val_lt_sub

Mathlib.Data.Fin.Basic

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

← MathLib Explorer

English

For Fin(n) with i ≤ j, (j−i).val < n−i.val.

Русский

Для Fin(n) при i ≤ j верно, что (j−i).val < n−i.val.

LaTeX

$$$$\forall n:\\mathbb{N},\forall i,j:\\mathrm{Fin}(n),\ i\le j \;\Rightarrow\; (j-i).\mathrm{val} < n - i.\mathrm{val}.$$$$

Lean4

theorem sub_val_lt_sub {n : ℕ} {i j : Fin n} (hij : i ≤ j) : (j - i).val < n - i.val := by
  simp [sub_val_of_le hij, Nat.sub_lt_sub_right hij j.isLt]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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