nhds

Mathlib.Topology.Filter

URI: https://scilib.ai/kg/mathlib#ContinuousAt.nhds

English

If f is continuous at x, then nhds ∘ f is continuous at x.

Русский

Если f непрерывна в точке x, то 𝓝 ∘ f непрерывна в точке x.

LaTeX

$$$\\text{ContinuousAt}(f,x)\\Rightarrow\\text{ContinuousAt}(\\mathcal{N}\\circ f,x)$$$

Lean4

protected nonrec theorem nhds (h : ContinuousAt f x) : ContinuousAt (𝓝 ∘ f) x :=
  h.nhds

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

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

Разделы

Аффилиация

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