val_add_one_of_lt' — Mathlib

English

Let n > 0 and i ∈ Fin(n) with i + 1 < n. Then the successor value satisfies (i + 1).val = i.val + 1.

Русский

Пусть n > 0 и i ∈ Fin(n) с условием i + 1 < n. Тогда значение следующего элемента равно значению i плюс 1: (i + 1).val = i.val + 1.

LaTeX

$$$ n > 0 \Rightarrow \forall i \in \mathrm{Fin}(n), i + 1 < n \Rightarrow (i + 1).\mathrm{val} = i.\mathrm{val} + 1 $$$

Lean4

theorem val_add_one_of_lt' {n : ℕ} [NeZero n] {i : Fin n} (h : i + 1 < n) : (i + 1).val = i.val + 1 := by
  simpa [add_def] using Nat.mod_eq_of_lt (by cutsat)

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