nodup_iff_injective_get — Mathlib

English

A vector's toList is nodup if and only if its get function is injective.

Русский

Список, получаемый из вектора, не содержит повторов тогда и только если функция get инъективна.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,n,\; v.toList\mathrm{Nodup} \iff \mathrm{Function.Injective}\ v.get$$$

Lean4

theorem nodup_iff_injective_get {v : Vector α n} : v.toList.Nodup ↔ Function.Injective v.get :=
  by
  obtain ⟨l, hl⟩ := v
  subst hl
  exact List.nodup_iff_injective_get

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