nodup_ofFn_ofInjective — Mathlib

English

If f: Fin n → α is injective, then ofFn f has no duplicates.

Русский

Если f: Fin n → α вводимая инъективна, то ofFn f не содержит повторов.

LaTeX

$$$$ \\text{If } f \\text{ is injective, then } \\operatorname{ofFn}(f) \\text{ is nodup}. $$$$

Lean4

theorem nodup_ofFn_ofInjective {n} {f : Fin n → α} (hf : Function.Injective f) : Nodup (ofFn f) :=
  by
  rw [ofFn_eq_pmap]
  exact nodup_range.pmap fun _ _ _ _ H => Fin.val_eq_of_eq <| hf H

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