getElem_bijective_iff — Mathlib

English

The bijectivity of the function n ↦ l[n] is equivalent to l.count a = 1 for all a.

Русский

Бижективность отображения n ↦ l[n] эквивалентна тому, что для каждого a верно count(a,l) = 1.

LaTeX

$$$ \forall {l}, [DecidableEq \alpha] \Rightarrow \operatorname{(Function.Bijective \; l.get)} \iff \forall a, \operatorname{count}(a,l) = 1 $$$

Lean4

theorem getElem_bijective_iff [DecidableEq α] : (fun (n : Fin l.length) ↦ l[n]).Bijective ↔ ∀ a, l.count a = 1 :=
  get_bijective_iff

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