nhds

Mathlib.Topology.Filter

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

English

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

Русский

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

LaTeX

$$$\\text{Continuous}(f)\\Rightarrow\\text{Continuous}(\\mathcal{N}\\circ f)$$$

Lean4

protected nonrec theorem nhds (h : Continuous f) : Continuous (𝓝 ∘ f) :=
  Filter.continuous_nhds.comp h

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

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

Разделы

Аффилиация

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