definitions with fin types (lean)

I try to formalize a few statements about geometry with the help of the great mathlib. Unfortunately I'm running into some issues expressing my definitions.

import analysis.convex.basic
import analysis.convex.segment
import algebra.module.basic
import data.set.basic
import data.list.basic
import data.fin.tuple.basic
open set

section polygon
variables R M : Type*
variables [ordered_semiring R] [add_comm_monoid M] [module R M]

definition PolygonChain {n : ℕ} (V: list (M, M)) (P : set M):
  ∀ pair ∈ V, (segment pair.0 pair.1) ⊆ P 
end polygon

What I want to say is, given a list of vertex tuples from some vector space (extreme points of a polygon chain) and a set of points (that is supposed to be the whole polygon chain), then there must be a segment between the start and end vertex from every tuple, in the set of all points from the polygon chain.

I tried different ways to build the definition and noticed, that I seem to misunderstand fin related types, so a more elaborate explanation, would be appreciated. More specific an alternative definition was

definition PolygonChain {n : ℕ} (V: vector M n) (P : set M): 
  ∀ m ∈ (fin n), (segment (vector.nth m) (vector.nth m+1)) ⊆ P

I know that that the forall quantor is only applicable to types (so it doesn't really iterate over the range 0 < n), and saying that sth. is an element of sth. else, isn't a valid notation for that. Moreover how would I in general express statements about ranges and specific entries in vectors and lists?

Edit: Thanks to Eric's answer I found the solution to the second definition

definition AltPolygonChain {n : ℕ} (v: vector M (n+1)) (P : set M): Prop := 
∀ m : fin (n), (segment R (vector.nth v m) (vector.nth v (m+1))) ⊆ P

Solution

This at least fixes the syntax errors in your code:

import analysis.convex.basic
import analysis.convex.segment
import algebra.module.basic
import data.set.basic
import data.list.basic
import data.fin.tuple.basic
open set

section polygon
variables R M : Type*
variables [ordered_semiring R] [add_comm_monoid M] [module R M]

definition PolygonChain {n : ℕ} (V: list (M × M)) (P : set M) : Prop :=
  ∀ pair : M × M, pair ∈ V → (segment R pair.1 pair.2) ⊆ P

end polygon

Some remarks:

list (M, M) should be spelt list (M × M). (a, b) is a term of type A × B.
The elements of a pair are .1 and .2, not .0 and .1.
Projection notation (.1) only works if Lean already knows the type of pair.
Segment needs an R argument.
If you're defining a property, you want def name : Prop := statement. If the statement appears before the :=, then you're proving the statement.