coeff_select — Mathlib

English

The sum of two selects with complementary predicates equals the original Witt vector: select P x + select (not P) x = x.

Русский

Сумма двух выборок с комплементарными предикатами даёт исходный Witt-вектор: select P x + select (¬P) x = x.

LaTeX

$$$ \text{select } P x + \text{select } (\lnot P) x = x $$$

Lean4

theorem coeff_select (x : 𝕎 R) (n : ℕ) : (select P x).coeff n = aeval x.coeff (selectPoly P n) :=
  by
  dsimp [select, selectPoly]
  split_ifs with hi <;> simp

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