DifferentiableWithinAtProp_self — Mathlib

English

From differentiability within at, we derive continuity within at.

Русский

Из дифференцируемости внутри множества следует непрерывность внутри множества.

LaTeX

$$$\text{MDifferentiableWithinAt } I I' f s x \Rightarrow \text{ContinuousWithinAt } f s x$$$

Lean4

theorem DifferentiableWithinAtProp_self {f : E → E'} {s : Set E} {x : E} :
    DifferentiableWithinAtProp 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  differentiableWithinAtProp_self_source

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