continuousWithinAt_diff_self — Mathlib

English

Removing a singleton from s does not change the continuity property at x: ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x.

Русский

Исключение единичного множества из s не изменяет свойство непрерывности в x: ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x.

LaTeX

$$$$\text{ContinuousWithinAt}(f, s \{x\}, x) \iff \text{ContinuousWithinAt}(f, s, x).$$$$

Lean4

/-- See also `continuousWithinAt_diff_singleton` for the case of `s \ {y}`, but
requiring `T1Space α. -/
@[simp]
theorem continuousWithinAt_diff_self : ContinuousWithinAt f (s \ { x }) x ↔ ContinuousWithinAt f s x :=
  continuousWithinAt_singleton.diff_iff

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