Topology on extended natural numbers

@[implicit_reducible]

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 ℕ∞

@[simp]

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

theorem ENat.isEmbedding_natCast : Topology.IsEmbedding Nat.cast

theorem ENat.isOpenEmbedding_natCast : Topology.IsOpenEmbedding 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

theorem ENat.tendsto_nhds_top_iff_natCast_lt {α : Type u_1} {l : Filter α} {f : α → ℕ∞} : Filter.Tendsto f l (nhds ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in l, ↑n < f a

instance ENat.instContinuousAdd : ContinuousAdd ℕ∞

instance ENat.instContinuousMul : ContinuousMul ℕ∞

theorem ENat.continuousAt_sub {a b : ℕ∞} (h : a ≠ ⊤ ∨ b ≠ ⊤) : ContinuousAt (Function.uncurry fun (x1 x2 : ℕ∞) => x1 - x2) (a, b)

theorem Filter.Tendsto.enatSub {α : Type u_1} {l : Filter α} {f g : α → ℕ∞} {a b : ℕ∞} (hf : Tendsto f l (nhds a)) (hg : Tendsto g l (nhds b)) (h : a ≠ ⊤ ∨ b ≠ ⊤) : Tendsto (fun (x : α) => f x - g x) l (nhds (a - b))

theorem ContinuousWithinAt.enatSub {X : Type u_1} [TopologicalSpace X] {f g : X → ℕ∞} {s : Set X} {x : X} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : f x ≠ ⊤ ∨ g x ≠ ⊤) : ContinuousWithinAt (fun (x : X) => f x - g x) s x

theorem ContinuousAt.enatSub {X : Type u_1} [TopologicalSpace X] {f g : X → ℕ∞} {x : X} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (h : f x ≠ ⊤ ∨ g x ≠ ⊤) : ContinuousAt (fun (x : X) => f x - g x) x

theorem ContinuousOn.enatSub {X : Type u_1} [TopologicalSpace X] {f g : X → ℕ∞} {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h : ∀ x ∈ s, f x ≠ ⊤ ∨ g x ≠ ⊤) : ContinuousOn (fun (x : X) => f x - g x) s

theorem Continuous.enatSub {X : Type u_1} [TopologicalSpace X] {f g : X → ℕ∞} (hf : Continuous f) (hg : Continuous g) (h : ∀ (x : X), f x ≠ ⊤ ∨ g x ≠ ⊤) : Continuous fun (x : X) => f x - g x