range_castSucc — Mathlib

English

The image of the castSucc map from Fin(n) to Fin(n+1) is exactly the set of elements of Fin(n+1) whose underlying value is less than n.

Русский

Образ отображения castSucc из Fin(n) в Fin(n+1) равен множеству элементов Fin(n+1) с числовым значением меньше n.

LaTeX

$$$$ \\mathrm{range}(\\operatorname{castSucc}) = \\{ x \\in \\mathrm{Fin}(n+1) : x \\text{ value } < n \\}. $$$$

Lean4

@[simp]
theorem range_castSucc {n : ℕ} : Set.range (castSucc : Fin n → Fin n.succ) = ({i | (i : ℕ) < n} : Set (Fin n.succ)) :=
  range_castLE (by cutsat)

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