continuousWithinAt — Mathlib

English

If HasGradientWithinAt f f' s x holds, then f is continuous on s at x in the sense of continuousWithinAt.

Русский

Градиент внутри множества гарантирует непрерывность на этом множестве в точке

LaTeX

$$HasGradientWithinAt f f' s x → ContinuousWithinAt f s x$$

Lean4

theorem continuousWithinAt (h : HasGradientWithinAt f f' s x) : ContinuousWithinAt f s x :=
  HasGradientAtFilter.tendsto_nhds inf_le_left h

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