approxOn_zero — Mathlib

English

For any measurable f, if we start the approximation sequence at n=0, the function F_0 equals the fixed point y0 (the chosen starting value).

Русский

Для любой измеримой функции f при аппроксимационной последовательности в начале (n=0) функция F_0 совпадает с заданной точкой y0.

LaTeX

$$$\\text{If } n=0:\\quad approxOn\\; f\\; hf\\; s\\; y_0\\; h_0\\; 0 = y_0.$$$

Lean4

@[simp]
theorem approxOn_zero {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s] (x : β) :
    approxOn f hf s y₀ h₀ 0 x = y₀ :=
  rfl

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