Naming a lemma for vector

Stream: new members

[Yakov Pechersky]

What would the name for the lemma in the example below me? I have a related lemma ported from list there for comparison.

import data.vector2

variables {α β : Type*} {n : ℕ} (v : vector α n) (x : α)

open vector

namespace vector

section pmap

variables {v x}
variables {p : α → Prop}

lemma nth_of_mem (h : x ∈ v.to_list) : ∃ i, v.nth i = x :=
mem_iff_nth.mp h

example : (∀ (i : fin n), p (v.nth i)) ↔ ∀ x ∈ v.to_list, p x :=
begin
  simp_rw mem_iff_nth,
  split,
  { rintros h x ⟨i, hi⟩,
    exact hi ▸ h i },
  { intros h i,
    refine h (v.nth i) ⟨i, rfl⟩ },
end

end pmap

[Yakov Pechersky]

With a golfed proof:

example : (∀ (i : fin n), p (v.nth i)) ↔ ∀ x ∈ v.to_list, p x :=
⟨λ h _ hx, exists.elim (nth_of_mem hx) (λ _ H, H ▸ h _), λ h i, h _ (mem_iff_nth.mpr ⟨i, rfl⟩)⟩

[Julian Berman]

well since no one else who knows what they're talking about chimed in I can throw stuff you maybe found already in :)

[Julian Berman]

namely with some grep skills, you found this list lemma right:

[Julian Berman]

https://github.com/leanprover-community/mathlib/blob/a027a37bfbd2805fa8b1cc6890b6edbcbb6648f7/src/data/list/of_fn.lean#L87-L89

[Julian Berman]

it looks like the closest signature in mathlib to what you have

[Julian Berman]

(so like forall_mem_of_nth_iff maybe, with the iff backwards?)

[Julian Berman]

I found that via rg --multiline '∀.*\n?.*↔.*∀.*' | rg fin after a few similar tries.

[Mario Carneiro]

I would suggest flipping the iff and calling it forall_mem_to_list_iff