continuousWithinAt — Mathlib

English

Any ContDiffWithinAt implies continuity of the function on the domain interior to s around x.

Русский

Любое ContDiffWithinAt влечет непрерывность функции на области внутри s вокруг x.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow ContinuousWithinAt f s x$$

Lean4

theorem continuousWithinAt (h : ContDiffWithinAt 𝕜 n f s x) : ContinuousWithinAt f s x :=
  by
  have := h.of_le (zero_le _)
  simp only [ContDiffWithinAt, nonpos_iff_eq_zero, Nat.cast_eq_zero, forall_eq, CharP.cast_eq_zero] at this
  rcases this with ⟨u, hu, p, H⟩
  rw [mem_nhdsWithin_insert] at hu
  exact (H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2

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