range_fin_succ — Mathlib

English

For any f : Fin(n+1) → α, the range of f equals the set insert (f(0)) (range (Fin.tail f)).

Русский

Для всякой функции f: Fin(n+1) → α область значений f равна множеству, образованному добавлением f(0) к образу хвоста: Set.range f = insert (f 0) (Set.range (Fin.tail f)).

LaTeX

$$$\\mathrm{Set.range}\,f = \\mathrm{Set.insert}\\bigl(f(0)\\bigr)\\bigl(\\mathrm{Set.range}(\\mathrm{Fin.tail}\,f)\\bigr).$$$

Lean4

theorem range_fin_succ {α} (f : Fin (n + 1) → α) : Set.range f = insert (f 0) (Set.range (Fin.tail f)) :=
  Set.ext fun _ ↦ exists_fin_succ.trans <| eq_comm.or Iff.rfl

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