continuousWithinAt_insert_self — Mathlib

English

Continuity within insert x s at x is equivalent to continuity within s at x.

Русский

Непрерывность внутри вставки x в s в точке x равна непрерывности внутри s в x.

LaTeX

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

Lean4

@[simp]
theorem continuousWithinAt_insert_self : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x := by
  simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and]

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