val_cast_of_lt — Mathlib

English

If a < n, then the value of the element a embedded into Fin n is a; i.e. (a : Fin n).val = a.

Русский

Если a < n, то значение элемента a, приведённого к Fin n, равно a; (a : Fin n).val = a.

LaTeX

$$$\\forall a,n \\in \\mathbb{N}, a < n \\Rightarrow (a : \\mathrm{Fin}(n)).\\mathrm{val} = a$$$

Lean4

/-- Converting an in-range number to `Fin (n + 1)` produces a result
whose value is the original number. -/
theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).val = a :=
  Nat.mod_eq_of_lt h

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