coord_apply_centroid — Mathlib

English

For a finite set s with i ∈ s, the coordinate at i of the centroid equals the reciprocal of the size of s.

Русский

Для конечного множества s с i ∈ s координата i у центроида равна обратному размеру s.

LaTeX

$$$ b.coord\\, i (s.centroid k b) = (|s| : k)^{-1}$ (при hi: i ∈ s)$$

Lean4

@[simp]
theorem coord_apply_centroid [CharZero k] (b : AffineBasis ι k P) {s : Finset ι} {i : ι} (hi : i ∈ s) :
    b.coord i (s.centroid k b) = (s.card : k)⁻¹ := by
  rw [Finset.centroid, b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]

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