select — Mathlib

English

The function x ↦ select P x is a polynomial function of Witt vector coefficients (in particular, P is a predicate on indices).

Русский

Функция x ↦ select P x является полиномиальной по коэффициентам Witt-вектора (P — предикат по индексам).

LaTeX

$$$ IsPoly p (\lambda _ _ x => select P x) $$$

Lean4

/-- `WittVector.select P x`, for a predicate `P : ℕ → Prop` is the Witt vector
whose `n`-th coefficient is `x.coeff n` if `P n` is true, and `0` otherwise.
-/
def select (P : ℕ → Prop) (x : 𝕎 R) : 𝕎 R :=
  mk p fun n => if P n then x.coeff n else 0

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