nhds_natCast

Mathlib.Topology.Instances.ENat

URI: https://scilib.ai/kg/mathlib#ENat.nhds_natCast

English

For every n ∈ ℕ, the neighborhood filter at n in ℕ∞ equals the pure filter at n.

Русский

Для каждого n ∈ ℕ, окрестностный фильтр в n для ℕ∞ равен чистому фильтру в n.

LaTeX

$$$$\\forall n \\in \\mathbb{N},\\; \\mathcal{N}(n) = \\operatorname{pure}(n).$$$$

Lean4

theorem nhds_natCast (n : ℕ) : 𝓝 (n : ℕ∞) = pure (n : ℕ∞) := by simp [← isOpenEmbedding_natCast.map_nhds_eq]

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

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

Разделы

Аффилиация

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