z — Mathlib · SciLib

English

The function z maps a Bernstein index k ∈ Fin(n+1) to the point k/n in the unit interval.

Русский

Функция z отображает индекс k ∈ Fin(n+1) в точку k/n на единичном отрезке.

LaTeX

$$$z(k) = \left( \dfrac{k}{n} , \text{proof of }0\le \dfrac{k}{n} \le 1 \right)$$$

Lean4

/-- Send `k : Fin (n+1)` to the equally spaced points `k/n` in the unit interval.
-/
def z {n : ℕ} (k : Fin (n + 1)) : I :=
  ⟨(k : ℝ) / n, by simp [div_nonneg, div_le_one_of_le₀, k.is_le]⟩

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