centroid_pair_fin — Mathlib

English

For p: Fin 2 → P, the centroid of univ is the midpoint between p(0) and p(1): (1/2)(p(1)-p(0)) added to p(0).

Русский

Для p: Fin 2 → P центр масс всех элементов равен полупрямой между p(0) и p(1): (1/2)(p(1) - p(0)) плюс p(0).

LaTeX

$$$\\mathrm{centroid}(k,\\mathrm{univ},p) = (2^{-1})\\cdot (p(1) - p(0)) + p(0)$$$

Lean4

/-- The centroid of two points indexed by `Fin 2`, expressed directly
as adding a vector to the first point. -/
theorem centroid_pair_fin [Invertible (2 : k)] (p : Fin 2 → P) : univ.centroid k p = (2⁻¹ : k) • (p 1 -ᵥ p 0) +ᵥ p 0 :=
  by
  rw [univ_fin2]
  convert centroid_pair k p 0 1

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