eval_at_0 — Mathlib

English

Evaluating Bernstein(n, ν) at 0 yields 1 if ν = 0 and 0 otherwise.

Русский

Значение Bernstein(n, ν) в 0 равно 1, если ν = 0, и 0 иначе.

LaTeX

$$$(\bernsteinPolynomial R n ν).eval 0 = \begin{cases}1 & \text{if } \nu = 0 \\ 0 & \text{otherwise} \end{cases}$$$

Lean4

theorem eval_at_0 (n ν : ℕ) : (bernsteinPolynomial R n ν).eval 0 = if ν = 0 then 1 else 0 :=
  by
  rw [bernsteinPolynomial]
  split_ifs with h
  · subst h; simp
  · simp [zero_pow h]

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