flip' — Mathlib

English

The Bernstein polynomial equals the composition with 1 − X of the Bernstein polynomial with the complementary index.

Русский

Полином Бернштейна равен композиции с 1 − X полинома Бернштейна с комплементарным индексом.

LaTeX

$$$\bernsteinPolynomial R n \nu = (\bernsteinPolynomial R n (n - \nu)).\mathrm{comp}(1 - X)$$$

Lean4

theorem flip' (n ν : ℕ) (h : ν ≤ n) : bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - X) := by
  simp [← flip _ _ _ h, Polynomial.comp_assoc]

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