flip — Mathlib

English

If ν ≤ n, then composing Bernstein(n, ν) with 1 − X yields Bernstein(n, n − ν).

Русский

При ν ≤ n составление Bernstein(n, ν) с 1 − X даёт Bernstein(n, n − ν).

LaTeX

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

Lean4

theorem flip (n ν : ℕ) (h : ν ≤ n) : (bernsteinPolynomial R n ν).comp (1 - X) = bernsteinPolynomial R n (n - ν) := by
  simp [bernsteinPolynomial, h, tsub_tsub_assoc, mul_right_comm]

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