ofFn_inj — Mathlib

English

For a fixed n, the map f,g : Fin n → α satisfies ofFn f = ofFn g iff f = g.

Русский

Фиксированно n, для функций f,g : Fin(n) → α верно, что ofFn f = ofFn g тогда и только тогда, когда f = g.

LaTeX

$$$\\forall n:\\ \\forall f,g:\\ Fin(n) \\to \\alpha,\\ \\operatorname{ofFn}(f) = \\operatorname{ofFn}(g) \\iff f = g.$$$

Lean4

/-- A special case of `List.ofFn_inj` for when the two functions are indexed by defeq `n`. -/
@[simp]
theorem ofFn_inj {n : ℕ} {f g : Fin n → α} : ofFn f = ofFn g ↔ f = g :=
  ofFn_injective.eq_iff

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