Topology on extended natural numbers

instance ENat.instTopologicalSpace : TopologicalSpace ℕ∞

Topology on ℕ∞.

Note: this is different from the EMetricSpace topology. The EMetricSpace topology has IsOpen {∞}, but all neighborhoods of ∞ in ℕ∞ contain infinite intervals.

Equations

• ENat.instTopologicalSpace = Preorder.topology ℕ∞

instance ENat.instOrderTopology : OrderTopology ℕ∞

Equations

• ENat.instOrderTopology = ⋯

@[simp]

theorem ENat.range_natCast : Set.range Nat.cast = Set.Iio ⊤

theorem ENat.embedding_natCast : Embedding Nat.cast

theorem ENat.openEmbedding_natCast : OpenEmbedding Nat.cast

theorem ENat.nhds_natCast (n : ℕ) : nhds ↑n = pure ↑n

@[simp]

theorem ENat.nhds_eq_pure {n : ℕ∞} (h : n ≠ ⊤) : nhds n = pure n

theorem ENat.isOpen_singleton {x : ℕ∞} (hx : x ≠ ⊤) : IsOpen {x}

theorem ENat.mem_nhds_iff {x : ℕ∞} {s : Set ℕ∞} (hx : x ≠ ⊤) : s ∈ nhds x ↔ x ∈ s

theorem ENat.mem_nhds_natCast_iff (n : ℕ) {s : Set ℕ∞} : s ∈ nhds ↑n ↔ ↑n ∈ s

instance ENat.instContinuousAdd : ContinuousAdd ℕ∞

Equations

• ENat.instContinuousAdd = ⋯