English
For any list l, l.get is bijective if and only if every element occurs exactly once in l.
Русский
Для любого списка l отображение l.get является биекцией тогда и только тогда каждый элемент встречается в l ровно один раз.
LaTeX
$$$ \forall {l},\ [DecidableEq \alpha] \Rightarrow \operatorname{l.get}.Bijective \iff \forall a, \operatorname{count}(a,l) = 1 $$$
Lean4
theorem get_bijective_iff [DecidableEq α] : l.get.Bijective ↔ ∀ a, l.count a = 1 :=
⟨fun h a ↦
(nodup_iff_count_eq_one.mp <| nodup_iff_injective_get.mpr h.injective) a <| mem_iff_get.mpr <| h.surjective a,
fun h ↦
⟨nodup_iff_injective_get.mp <| nodup_iff_count_eq_one.mpr fun a _ ↦ h a, fun a ↦
mem_iff_get.mp <| List.one_le_count_iff.mp <| by grind⟩⟩
