centerMass_singleton — Mathlib

English

The centerMass of a singleton equals the single point, provided the weight is nonzero.

Русский

Центр массы синглтона равен самой точке, если вес не равен нулю.

LaTeX

$$$\\text{centerMass of }\\{i\\}\\text{ with } w_i\\neq 0\\text{ equals } z_i.$$$

Lean4

theorem centerMass_singleton (hw : w i ≠ 0) : ({ i } : Finset ι).centerMass w z = z i :=
  by
  rw [centerMass, sum_singleton, sum_singleton]
  match_scalars
  field_simp

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