nodup_ofFn — Mathlib

English

Nodup (ofFn f) holds iff f is injective.

Русский

Nodup (ofFn f) эквивалентно тому, что f инъективна.

LaTeX

$$$$ \\operatorname{Nodup}(\\operatorname{ofFn}(f)) \\;\\iff\\; \\text{Injective}(f). $$$$

Lean4

theorem nodup_ofFn {n} {f : Fin n → α} : Nodup (ofFn f) ↔ Function.Injective f :=
  by
  refine ⟨?_, nodup_ofFn_ofInjective⟩
  refine Fin.consInduction ?_ (fun x₀ xs ih => ?_) f
  · intro _
    exact Function.injective_of_subsingleton _
  · intro h
    rw [Fin.cons_injective_iff]
    simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
    exact h.imp_right ih

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