mkD_of_not_continuousOn — Mathlib

English

If f is not continuous on s, then mkD on the restricted function equals g.

Русский

Если f не непрерывна на s, то mkD на ограниченной функции равняется g.

LaTeX

$$mkD((s.restrict f), g) = g$$

Lean4

theorem mkD_of_not_continuousOn {s : Set X} [Zero s] {f : X → R} {g : C(s, R)₀} (hf : ¬ContinuousOn f s) :
    mkD (s.restrict f) g = g := by
  rw [continuousOn_iff_continuous_restrict] at hf
  exact mkD_of_not_continuous hf

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