continuousWithinAt_compl_self — Mathlib

English

Continuity within the complement of a singleton at x is equivalent to ordinary continuity at x.

Русский

Непрерывность внутри дополнения единичного множества равна обычной непрерывности в точке x.

LaTeX

$$$$\text{ContinuousWithinAt}(f, \{x\}^c, x) \iff \text{ContinuousAt}(f, x).$$$$

Lean4

@[simp]
theorem continuousWithinAt_compl_self : ContinuousWithinAt f { x }ᶜ x ↔ ContinuousAt f x := by
  rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]

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