continuousWithinAt_singleton

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#continuousWithinAt_singleton

← MathLib Explorer

English

For any x, f is continuous within the singleton {x} at x.

Русский

Для любого x функция f непрерывна на синглетоне {x} в точке x.

LaTeX

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

Lean4

@[simp]
theorem continuousWithinAt_singleton : ContinuousWithinAt f { x } x := by
  simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru