mkD_apply_of_continuousOn — Mathlib

English

For x in s, mkD on s.restrict f applied to x equals f(x).

Русский

Для x ∈ s, mkD на s.restrict f применимо к x и даёт f(x).

LaTeX

$$mkD((s.restrict f), g)(x) = f(x) \\quad (x \\in s)$$

Lean4

theorem mkD_apply_of_continuousOn {s : Set X} [Zero s] {f : X → R} {g : C(s, R)₀} {x : s} (hf : ContinuousOn f s)
    (hf₀ : f (0 : s) = 0) : mkD (s.restrict f) g x = f x := by
  rw [mkD_of_continuousOn hf hf₀, coe_mk, ContinuousMap.coe_mk, restrict_apply]

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