continuousWithinAt_of_notMem_closure

English

If x is not in the closure of s, then f is continuous within s at x.

Русский

Если x не принадлежит замыканию множества s, то f непрерывна внутри s в точке x.

LaTeX

$$$x \\notin \\overline{s} \\Rightarrow ContinuousWithinAt\\ f\\ s\\ x$$$

Lean4

theorem continuousWithinAt_of_notMem_closure (hx : x ∉ closure s) : ContinuousWithinAt f s x :=
  by
  rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
  rw [ContinuousWithinAt, hx]
  exact tendsto_bot

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