English
The oscillation within D at x is zero if and only if f is continuous within D at x, provided x is in D.
Русский
Осцилляция внутри D в x равна нулю тогда и только тогда, когда f непрерывна внутри D в x, при условии x ∈ D.
LaTeX
$$$\\operatorname{oscillationWithin}(f,D,x)=0 \\iff x\\in D \\land \\operatorname{ContinuousWithinAt}(f,D,x)$$
Lean4
/-- The oscillation within `D` of `f` at `x ∈ D` is 0 if and only if `ContinuousWithinAt f D x`. -/
theorem eq_zero_iff_continuousWithinAt [TopologicalSpace E] (f : E → F) {D : Set E} {x : E} (xD : x ∈ D) :
oscillationWithin f D x = 0 ↔ ContinuousWithinAt f D x :=
by
refine ⟨fun hf ↦ EMetric.tendsto_nhds.mpr (fun ε ε0 ↦ ?_), fun hf ↦ hf.oscillationWithin_eq_zero⟩
simp_rw [← hf, oscillationWithin, iInf_lt_iff] at ε0
obtain ⟨S, hS, Sε⟩ := ε0
refine Filter.mem_of_superset hS (fun y hy ↦ lt_of_le_of_lt ?_ Sε)
exact edist_le_diam_of_mem (mem_preimage.1 hy) <| mem_preimage.1 (mem_of_mem_nhdsWithin xD hS)
