contDiffWithinAt_zero — Mathlib

English

Equivalent to 43934: ContDiffOn 𝕜 0 f s ↔ ContinuousOn f s.

Русский

Эквивалентно 43934: ContDiffOn 𝕜 0 f s ⇔ ContinuousOn f s.

LaTeX

$$$ContDiffOn\\ 𝕜\\ 0\\ f\\ s\\ \\leftrightarrow\\ ContinuousOn\\ f\\ s$$$

Lean4

theorem contDiffWithinAt_zero (hx : x ∈ s) : ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u) :=
  by
  constructor
  · intro h
    obtain ⟨u, H, p, hp⟩ := h 0 le_rfl
    refine ⟨u, ?_, ?_⟩
    · simpa [hx] using H
    · simp only [Nat.cast_zero, hasFTaylorSeriesUpToOn_zero_iff] at hp
      exact hp.1.mono inter_subset_right
  · rintro ⟨u, H, hu⟩
    rw [← contDiffWithinAt_inter' H]
    have h' : x ∈ s ∩ u := ⟨hx, mem_of_mem_nhdsWithin hx H⟩
    exact (contDiffOn_zero.mpr hu).contDiffWithinAt h'

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