ext_elem — Mathlib

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]

Похожие утверждения