English
The centroid of two points is their midpoint: the centroid of {i1,i2} is p(i1) + (1/2)(p(i2) - p(i1)).
Русский
Центроид пары точек равен их середине: центроид {i1,i2} = p(i1) + (1/2)(p(i2) - p(i1)).
LaTeX
$$$\\mathrm{centroid}(k,\\{i_1,i_2\\},p) = p(i_1) + \\tfrac{1}{2}\\,(p(i_2) - p(i_1))$$$
Lean4
/-- The centroid of two points, expressed directly as adding a vector
to a point. -/
theorem centroid_pair [DecidableEq ι] [Invertible (2 : k)] (p : ι → P) (i₁ i₂ : ι) :
({ i₁, i₂ } : Finset ι).centroid k p = (2⁻¹ : k) • (p i₂ -ᵥ p i₁) +ᵥ p i₁ :=
by
by_cases h : i₁ = i₂
· simp [h]
· have hc : (#{ i₁, i₂ } : k) ≠ 0 :=
by
rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]
norm_num
exact Invertible.ne_zero _
rw [centroid_def,
affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
(sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
simp [h, one_add_one_eq_two]
