eval_at_1 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem eval_at_1 (n ν : ℕ) : (bernsteinPolynomial R n ν).eval 1 = if ν = n then 1 else 0 :=
  by
  rw [bernsteinPolynomial]
  split_ifs with h
  · subst h; simp
  · obtain hνn | hnν := Ne.lt_or_gt h
    · simp [zero_pow <| Nat.sub_ne_zero_of_lt hνn]
    · simp [Nat.choose_eq_zero_of_lt hnν]

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