centerMass_filter_ne_zero — Mathlib

English

Dropping indices with zero weight from the center of mass does not change the result.

Русский

Исключение индексов с нулевым весом из центра массы не изменяет результат.

LaTeX

$${i ∈ t | w_i ≠ 0}.centerMass\, w\, z = t.centerMass\, w\, z$$

Lean4

theorem centerMass_filter_ne_zero [∀ i, Decidable (w i ≠ 0)] : {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z :=
  Finset.centerMass_subset z (filter_subset _ _) fun i hit hit' => by
    simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'

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