基于Lean/mathlib的多边形链定义问题及fin类型疑惑

问题背景 #

我尝试借助mathlib库形式化若干几何语句，但在定义表达上遇到了问题。

最初的定义代码 #

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

我的意图是：给定向量空间中的顶点元组列表（多边形链的端点）和一个点集（代表整个多边形链），要求每个元组的起始顶点与结束顶点之间的线段都包含在该点集中。

尝试的其他定义及困惑 #

我尝试了多种定义方式，发现自己对fin相关类型存在误解，希望能得到详细讲解。曾尝试的另一种定义如下：

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

我知道forall量词仅适用于类型（无法真正遍历0 < n的范围），且“某元素属于某类型”的写法并不合法。此外，我想了解如何在Lean中表达关于向量和列表的范围及特定元素的通用语句。

最终解决的定义 #

编辑：感谢Eric的解答，我找到了第二种定义的解决方案：

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

内容的提问来源于stack exchange，提问作者n-0