nhds

Mathlib.Topology.Filter

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

English

If f is continuous on s, then nhds ∘ f is continuous on s.

Русский

Если f непрерывна на множестве s, то 𝓝 ∘ f непрерывна на s.

LaTeX

$$$\\text{ContinuousOn}(f,s)\\Rightarrow\\text{ContinuousOn}(\\mathcal{N}\\circ f,s)$$$

Lean4

protected nonrec theorem nhds (h : ContinuousOn f s) : ContinuousOn (𝓝 ∘ f) s := fun x hx => (h x hx).nhds

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

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

Разделы

Аффилиация

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