mem_nhds_natCast_iff

Mathlib.Topology.Instances.ENat

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

English

For every natural number n, and s ⊆ ENat, s ∈ nhds(n.cast) iff n.cast ∈ s.

Русский

Для каждого натурального числа n и множества s, s ∈ nhds(n.cast) ⇔ n.cast ∈ s.

LaTeX

$$$$\\forall n \\in \\mathbb{N},\\; s \\in \\mathcal{N}(n.cast) \\iff n.cast \\in s.$$$$

Lean4

theorem mem_nhds_natCast_iff (n : ℕ) {s : Set ℕ∞} : s ∈ 𝓝 (n : ℕ∞) ↔ (n : ℕ∞) ∈ s :=
  mem_nhds_iff (coe_ne_top _)

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

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

Разделы

Аффилиация

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