oscillationWithin_eq_zero — Mathlib

English

If f is continuously within a set D at x, then the oscillation of f over D at x is zero.

Русский

Пусть f непрерывна внутри множества D в точке x. Тогда осцилляция f на D в точке x равна 0.

LaTeX

$$$\\text{ContinuousWithinAt}(f,D,x) \\;\Rightarrow\\; \\operatorname{oscillationWithin}(f,D,x)=0$$$

Lean4

theorem oscillationWithin_eq_zero [TopologicalSpace E] {f : E → F} {D : Set E} {x : E} (hf : ContinuousWithinAt f D x) :
    oscillationWithin f D x = 0 :=
  by
  refine le_antisymm (_root_.le_of_forall_pos_le_add fun ε hε ↦ ?_) (zero_le _)
  rw [zero_add]
  have : ball (f x) (ε / 2) ∈ (𝓝[D] x).map f := hf <| ball_mem_nhds _ (by simp [ne_of_gt hε])
  refine (biInf_le diam this).trans (le_of_le_of_eq diam_ball ?_)
  exact (ENNReal.mul_div_cancel (by simp) (by simp))

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