English
If the coordinates of two points q1 and q2 are equal with respect to every index i in ι, then q1 = q2 (assuming finite ι).
Русский
Если координаты двух точек q1 и q2 совпадают по всем индексам i из ι, то q1 = q2 (при условии конечности ι).
LaTeX
$$$\\forall q_1,q_2,\\; (\\forall i,\\ b.coord\\, i\\; q_1 = b.coord\\, i\\; q_2) \\Rightarrow q_1 = q_2$$$
Lean4
theorem ext_elem [Finite ι] {q₁ q₂ : P} (h : ∀ i, b.coord i q₁ = b.coord i q₂) : q₁ = q₂ :=
by
cases nonempty_fintype ι
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]
simp only [h]