feat: port Topology.Instances.Ereal (#2796)

### API changes

- Add `ENNReal.range_coe`, `ENNReal.range_coe'`, and `ENNReal.coe_strictMono`.
- Add instances for `DenselyOrdered EReal`, `T5Space EReal`, `ContinuousNeg EReal`, and `CanLift EReal ENNReal _ _`.
- Add `EReal.range_coe`, `EReal.range_coe_eq_Ioo`, `EReal.range_coe_ennreal`.
- Add `EReal.denseRange_ratCast`, `EReal.nhds_top_basis`, `EReal.nhds_bot_basis`.
- Deprecate `EReal.negHomeo` and `EReal.continuous_neg`.
- Generalize `orderTopology_of_ordConnected` to `StrictMono.induced_topology_eq_preorder` and `StrictMono.embedding_of_ordConnected`, use it to prove that some coercions are embeddings.
- Prove `TopologicalSpace.SecondCountableTopology.of_separableSpace_orderTopology` and helper lemmas `Dense.topology_eq_generateFrom`, `Dense.Ioi_eq_bunionᵢ`, and `Dense.Iio_eq_bunionᵢ`.

Mathlib.lean

@@ -1436,6 +1436,7 @@ import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Homotopy.Basic
 import Mathlib.Topology.Inseparable
 import Mathlib.Topology.Instances.ENNReal
+import Mathlib.Topology.Instances.EReal
 import Mathlib.Topology.Instances.Int
 import Mathlib.Topology.Instances.NNReal
 import Mathlib.Topology.Instances.Nat

Mathlib/Data/Real/ENNReal.lean

@@ -10,6 +10,7 @@ Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Data.Real.NNReal
 import Mathlib.Algebra.Order.Sub.WithTop
+import Mathlib.Data.Set.Intervals.WithBotTop
 
 /-!
 # Extended non-negative reals
@@ -152,6 +153,9 @@ instance canLift : CanLift ℝ≥0∞ ℝ≥0 some (· ≠ ∞) := WithTop.canLi
 
 @[simp] theorem some_eq_coe' (a : ℝ≥0) : (WithTop.some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl
 
+theorem range_coe' : range some = Iio ∞ := WithTop.range_coe
+theorem range_coe : range some = {∞}ᶜ := (isCompl_range_some_none ℝ≥0).symm.compl_eq.symm
+
 /-- `to_nnreal x` returns `x` if it is real, otherwise 0. -/
 protected def toNNReal : ℝ≥0∞ → ℝ≥0 := WithTop.untop' 0
 #align ennreal.to_nnreal ENNReal.toNNReal
@@ -317,6 +321,8 @@ theorem toReal_eq_one_iff (x : ℝ≥0∞) : x.toReal = 1 ↔ x = 1 := by
 theorem coe_mono : Monotone some := fun _ _ => coe_le_coe.2
 #align ennreal.coe_mono ENNReal.coe_mono
 
+theorem coe_strictMono : StrictMono some := fun _ _ => coe_lt_coe.2
+
 @[simp, norm_cast] theorem coe_eq_zero : (↑r : ℝ≥0∞) = 0 ↔ r = 0 := coe_eq_coe
 #align ennreal.coe_eq_zero ENNReal.coe_eq_zero
 

Mathlib/Data/Real/EReal.lean

@@ -52,7 +52,7 @@ if and only if they have the same absolute value and the same sign.
 real, ereal, complete lattice
 -/
 
-open Function ENNReal NNReal
+open Function ENNReal NNReal Set
 
 noncomputable section
 
@@ -71,6 +71,9 @@ instance : CompleteLinearOrder EReal :=
 instance : LinearOrderedAddCommMonoid EReal :=
   inferInstanceAs (LinearOrderedAddCommMonoid (WithBot (WithTop ℝ)))
 
+instance : DenselyOrdered EReal :=
+  inferInstanceAs (DenselyOrdered (WithBot (WithTop ℝ)))
+
 /-- The canonical inclusion froms reals to ereals. Registered as a coercion. -/
 @[coe] def Real.toEReal : ℝ → EReal := some ∘ some
 #align real.to_ereal Real.toEReal
@@ -339,6 +342,14 @@ theorem top_ne_zero : (⊤ : EReal) ≠ 0 :=
   (coe_ne_top 0).symm
 #align ereal.top_ne_zero EReal.top_ne_zero
 
+theorem range_coe : range Real.toEReal = {⊥, ⊤}ᶜ := by
+  ext x
+  induction x using EReal.rec <;> simp
+
+theorem range_coe_eq_Ioo : range Real.toEReal = Ioo ⊥ ⊤ := by
+  ext x
+  induction x using EReal.rec <;> simp
+
 @[simp, norm_cast]
 theorem coe_add (x y : ℝ) : (↑(x + y) : EReal) = x + y :=
   rfl
@@ -529,6 +540,14 @@ theorem coe_ennreal_nonneg (x : ℝ≥0∞) : (0 : EReal) ≤ x :=
   coe_ennreal_le_coe_ennreal_iff.2 (zero_le x)
 #align ereal.coe_ennreal_nonneg EReal.coe_ennreal_nonneg
 
+@[simp] theorem range_coe_ennreal : range ((↑) : ℝ≥0∞ → EReal) = Set.Ici 0 :=
+  Subset.antisymm (range_subset_iff.2 coe_ennreal_nonneg) fun x => match x with
+    | ⊥ => fun h => absurd h bot_lt_zero.not_le
+    | ⊤ => fun _ => ⟨⊤, rfl⟩
+    | (x : ℝ) => fun h => ⟨.some ⟨x, EReal.coe_nonneg.1 h⟩, rfl⟩
+
+instance : CanLift EReal ℝ≥0∞ (↑) (0 ≤ ·) := ⟨range_coe_ennreal.ge⟩
+
 @[simp, norm_cast]
 theorem coe_ennreal_pos {x : ℝ≥0∞} : (0 : EReal) < x ↔ 0 < x := by
   rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]

Mathlib/Topology/Instances/ENNReal.lean

@@ -50,11 +50,8 @@ instance : NormalSpace ℝ≥0∞ := inferInstance
 instance : SecondCountableTopology ℝ≥0∞ :=
   orderIsoUnitIntervalBirational.toHomeomorph.embedding.secondCountableTopology
 
-theorem embedding_coe : Embedding ((↑) : ℝ≥0 → ℝ≥0∞) := by
-  refine ⟨⟨OrderTopology.topology_eq_generate_intervals.trans ?_⟩, fun _ _ => coe_eq_coe.1⟩
-  refine (induced_topology_eq_preorder coe_lt_coe (fun h _ => ?_) fun h _ => ?_).symm <;>
-    rcases lt_iff_exists_nnreal_btwn.1 h with ⟨a, h₁, h₂⟩
-  exacts [⟨a, coe_lt_coe.1 h₂, h₁.le⟩, ⟨a, coe_lt_coe.1 h₁, h₂.le⟩]
+theorem embedding_coe : Embedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
+  coe_strictMono.embedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio
 #align ennreal.embedding_coe ENNReal.embedding_coe
 
 theorem isOpen_ne_top : IsOpen { a : ℝ≥0∞ | a ≠ ⊤ } := isOpen_ne
@@ -66,9 +63,7 @@ theorem isOpen_Ico_zero : IsOpen (Ico 0 b) := by
 #align ennreal.is_open_Ico_zero ENNReal.isOpen_Ico_zero
 
 theorem openEmbedding_coe : OpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
-  ⟨embedding_coe, by
-    convert isOpen_ne_top
-    ext (x | _) <;> simp [none_eq_top, some_eq_coe]⟩
+  ⟨embedding_coe, by rw [range_coe']; exact isOpen_Iio⟩
 #align ennreal.open_embedding_coe ENNReal.openEmbedding_coe
 
 theorem coe_range_mem_nhds : range ((↑) : ℝ≥0 → ℝ≥0∞) ∈ 𝓝 (r : ℝ≥0∞) :=

Mathlib/Topology/Instances/EReal.lean

@@ -0,0 +1,258 @@
+/-
+Copyright (c) 2021 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+
+! This file was ported from Lean 3 source module topology.instances.ereal
+! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Rat.Encodable
+import Mathlib.Data.Real.EReal
+import Mathlib.Topology.Algebra.Order.MonotoneContinuity
+import Mathlib.Topology.Instances.ENNReal
+
+/-!
+# Topological structure on `EReal`
+
+We endow `EReal` with the order topology, and prove basic properties of this topology.
+
+## Main results
+
+* `Real.toEReal : ℝ → EReal` is an open embedding
+* `ENNReal.toEReal : ℝ≥0∞ → EReal` is a closed embedding
+* The addition on `EReal` is continuous except at `(⊥, ⊤)` and at `(⊤, ⊥)`.
+* Negation is a homeomorphism on `EReal`.
+
+## Implementation
+
+Most proofs are adapted from the corresponding proofs on `ℝ≥0∞`.
+-/
+
+
+noncomputable section
+
+open Classical Set Filter Metric TopologicalSpace Topology
+open scoped ENNReal NNReal BigOperators Filter
+
+variable {α : Type _} [TopologicalSpace α]
+
+namespace EReal
+
+instance : TopologicalSpace EReal := Preorder.topology EReal
+instance : OrderTopology EReal := ⟨rfl⟩
+instance : T5Space EReal := inferInstance
+instance : T2Space EReal := inferInstance
+
+lemma denseRange_ratCast : DenseRange (fun r : ℚ ↦ ((r : ℝ) : EReal)) :=
+  dense_of_exists_between fun _ _ h => exists_range_iff.2 <| exists_rat_btwn_of_lt h
+
+instance : SecondCountableTopology EReal :=
+  have : SeparableSpace EReal := ⟨⟨_, countable_range _, denseRange_ratCast⟩⟩
+  .of_separableSpace_orderTopology _
+
+/-! ### Real coercion -/
+
+theorem embedding_coe : Embedding ((↑) : ℝ → EReal) :=
+  coe_strictMono.embedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo
+#align ereal.embedding_coe EReal.embedding_coe
+
+theorem openEmbedding_coe : OpenEmbedding ((↑) : ℝ → EReal) :=
+  ⟨embedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩
+#align ereal.open_embedding_coe EReal.openEmbedding_coe
+
+@[norm_cast]
+theorem tendsto_coe {α : Type _} {f : Filter α} {m : α → ℝ} {a : ℝ} :
+    Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
+  embedding_coe.tendsto_nhds_iff.symm
+#align ereal.tendsto_coe EReal.tendsto_coe
+
+theorem _root_.continuous_coe_real_ereal : Continuous ((↑) : ℝ → EReal) :=
+  embedding_coe.continuous
+#align continuous_coe_real_ereal continuous_coe_real_ereal
+
+theorem continuous_coe_iff {f : α → ℝ} : (Continuous fun a => (f a : EReal)) ↔ Continuous f :=
+  embedding_coe.continuous_iff.symm
+#align ereal.continuous_coe_iff EReal.continuous_coe_iff
+
+theorem nhds_coe {r : ℝ} : 𝓝 (r : EReal) = (𝓝 r).map (↑) :=
+  (openEmbedding_coe.map_nhds_eq r).symm
+#align ereal.nhds_coe EReal.nhds_coe
+
+theorem nhds_coe_coe {r p : ℝ} :
+    𝓝 ((r : EReal), (p : EReal)) = (𝓝 (r, p)).map fun p : ℝ × ℝ => (↑p.1, ↑p.2) :=
+  ((openEmbedding_coe.prod openEmbedding_coe).map_nhds_eq (r, p)).symm
+#align ereal.nhds_coe_coe EReal.nhds_coe_coe
+
+theorem tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
+    Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal) := by
+  lift a to ℝ using ⟨ha, h'a⟩
+  rw [nhds_coe, tendsto_map'_iff]
+  exact tendsto_id
+#align ereal.tendsto_to_real EReal.tendsto_toReal
+
+theorem continuousOn_toReal : ContinuousOn EReal.toReal ({⊥, ⊤}ᶜ : Set EReal) := fun _a ha =>
+  ContinuousAt.continuousWithinAt (tendsto_toReal (mt Or.inr ha) (mt Or.inl ha))
+#align ereal.continuous_on_to_real EReal.continuousOn_toReal
+
+/-- The set of finite `EReal` numbers is homeomorphic to `ℝ`. -/
+def neBotTopHomeomorphReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ₜ ℝ where
+  toEquiv := neTopBotEquivReal
+  continuous_toFun := continuousOn_iff_continuous_restrict.1 continuousOn_toReal
+  continuous_invFun := continuous_coe_real_ereal.subtype_mk _
+#align ereal.ne_bot_top_homeomorph_real EReal.neBotTopHomeomorphReal
+
+/-! ### ennreal coercion -/
+
+theorem embedding_coe_ennreal : Embedding ((↑) : ℝ≥0∞ → EReal) :=
+  coe_ennreal_strictMono.embedding_of_ordConnected <| by
+    rw [range_coe_ennreal]; exact ordConnected_Ici
+#align ereal.embedding_coe_ennreal EReal.embedding_coe_ennreal
+
+theorem closedEmbedding_coe_ennreal : ClosedEmbedding ((↑) : ℝ≥0∞ → EReal) :=
+  ⟨embedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩
+
+@[norm_cast]
+theorem tendsto_coe_ennreal {α : Type _} {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
+    Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) :=
+  embedding_coe_ennreal.tendsto_nhds_iff.symm
+#align ereal.tendsto_coe_ennreal EReal.tendsto_coe_ennreal
+
+theorem _root_.continuous_coe_ennreal_ereal : Continuous ((↑) : ℝ≥0∞ → EReal) :=
+  embedding_coe_ennreal.continuous
+#align continuous_coe_ennreal_ereal continuous_coe_ennreal_ereal
+
+theorem continuous_coe_ennreal_iff {f : α → ℝ≥0∞} :
+    (Continuous fun a => (f a : EReal)) ↔ Continuous f :=
+  embedding_coe_ennreal.continuous_iff.symm
+#align ereal.continuous_coe_ennreal_iff EReal.continuous_coe_ennreal_iff
+
+/-! ### Neighborhoods of infinity -/
+
+theorem nhds_top : 𝓝 (⊤ : EReal) = ⨅ (a) (_h : a ≠ ⊤), 𝓟 (Ioi a) :=
+  nhds_top_order.trans <| by simp only [lt_top_iff_ne_top]
+#align ereal.nhds_top EReal.nhds_top
+
+nonrec theorem nhds_top_basis : (𝓝 (⊤ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Ioi ·) := by
+  refine nhds_top_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, coe_lt_top _, Subset.rfl⟩
+  rcases exists_rat_btwn_of_lt hx with ⟨y, hxy, -⟩
+  exact ⟨_, trivial, Ioi_subset_Ioi hxy.le⟩
+
+theorem nhds_top' : 𝓝 (⊤ : EReal) = ⨅ a : ℝ, 𝓟 (Ioi ↑a) := nhds_top_basis.eq_infᵢ
+#align ereal.nhds_top' EReal.nhds_top'
+
+theorem mem_nhds_top_iff {s : Set EReal} : s ∈ 𝓝 (⊤ : EReal) ↔ ∃ y : ℝ, Ioi (y : EReal) ⊆ s :=
+  nhds_top_basis.mem_iff.trans <| by simp only [true_and]
+#align ereal.mem_nhds_top_iff EReal.mem_nhds_top_iff
+
+theorem tendsto_nhds_top_iff_real {α : Type _} {m : α → EReal} {f : Filter α} :
+    Tendsto m f (𝓝 ⊤) ↔ ∀ x : ℝ, ∀ᶠ a in f, ↑x < m a :=
+  nhds_top_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Ioi]
+#align ereal.tendsto_nhds_top_iff_real EReal.tendsto_nhds_top_iff_real
+
+theorem nhds_bot : 𝓝 (⊥ : EReal) = ⨅ (a) (_h : a ≠ ⊥), 𝓟 (Iio a) :=
+  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]
+#align ereal.nhds_bot EReal.nhds_bot
+
+theorem nhds_bot_basis : (𝓝 (⊥ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Iio ·) := by
+  refine nhds_bot_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩
+  rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩
+  exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩
+
+theorem nhds_bot' : 𝓝 (⊥ : EReal) = ⨅ a : ℝ, 𝓟 (Iio ↑a) :=
+  nhds_bot_basis.eq_infᵢ
+#align ereal.nhds_bot' EReal.nhds_bot'
+
+theorem mem_nhds_bot_iff {s : Set EReal} : s ∈ 𝓝 (⊥ : EReal) ↔ ∃ y : ℝ, Iio (y : EReal) ⊆ s :=
+  nhds_bot_basis.mem_iff.trans <| by simp only [true_and]
+#align ereal.mem_nhds_bot_iff EReal.mem_nhds_bot_iff
+
+theorem tendsto_nhds_bot_iff_real {α : Type _} {m : α → EReal} {f : Filter α} :
+    Tendsto m f (𝓝 ⊥) ↔ ∀ x : ℝ, ∀ᶠ a in f, m a < x :=
+  nhds_bot_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Iio]
+#align ereal.tendsto_nhds_bot_iff_real EReal.tendsto_nhds_bot_iff_real
+
+/-! ### Continuity of addition -/
+
+theorem continuousAt_add_coe_coe (a b : ℝ) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, b) := by
+  simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, (· ∘ ·), tendsto_coe,
+    tendsto_add]
+#align ereal.continuous_at_add_coe_coe EReal.continuousAt_add_coe_coe
+
+theorem continuousAt_add_top_coe (a : ℝ) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, a) := by
+  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]
+  refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
+    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_
+  simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
+#align ereal.continuous_at_add_top_coe EReal.continuousAt_add_top_coe
+
+theorem continuousAt_add_coe_top (a : ℝ) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, ⊤) := by
+  simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap]
+    using Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))
+#align ereal.continuous_at_add_coe_top EReal.continuousAt_add_coe_top
+
+theorem continuousAt_add_top_top : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊤, ⊤) := by
+  simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
+  refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
+    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
+  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
+#align ereal.continuous_at_add_top_top EReal.continuousAt_add_top_top
+
+theorem continuousAt_add_bot_coe (a : ℝ) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, a) := by
+  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
+  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
+    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_
+  simpa only [← coe_add, sub_add_cancel] using add_lt_add h.1 h.2
+#align ereal.continuous_at_add_bot_coe EReal.continuousAt_add_bot_coe
+
+theorem continuousAt_add_coe_bot (a : ℝ) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, ⊥) := by
+  simpa only [add_comm, (· ∘ ·), ContinuousAt, Prod.swap]
+    using Tendsto.comp (continuousAt_add_bot_coe a) (continuous_swap.tendsto ((a : EReal), ⊥))
+#align ereal.continuous_at_add_coe_bot EReal.continuousAt_add_coe_bot
+
+theorem continuousAt_add_bot_bot : ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (⊥, ⊥) := by
+  simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
+  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe 0)).prod_nhds
+    (gt_mem_nhds <| bot_lt_coe r)).mono fun _ h ↦ ?_
+  simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2
+#align ereal.continuous_at_add_bot_bot EReal.continuousAt_add_bot_bot
+
+/-- The addition on `EReal` is continuous except where it doesn't make sense (i.e., at `(⊥, ⊤)`
+and at `(⊤, ⊥)`). -/
+theorem continuousAt_add {p : EReal × EReal} (h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥) (h' : p.1 ≠ ⊥ ∨ p.2 ≠ ⊤) :
+    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) p := by
+  rcases p with ⟨x, y⟩
+  induction x using EReal.rec <;> induction y using EReal.rec
+  · exact continuousAt_add_bot_bot
+  · exact continuousAt_add_bot_coe _
+  · simp at h'
+  · exact continuousAt_add_coe_bot _
+  · exact continuousAt_add_coe_coe _ _
+  · exact continuousAt_add_coe_top _
+  · simp at h
+  · exact continuousAt_add_top_coe _
+  · exact continuousAt_add_top_top
+#align ereal.continuous_at_add EReal.continuousAt_add
+
+/-! ### Negation -/
+
+instance : ContinuousNeg EReal := ⟨negOrderIso.continuous⟩
+
+/-- Negation on `EReal` as a homeomorphism -/
+@[deprecated Homeomorph.neg]
+def negHomeo : EReal ≃ₜ EReal :=
+  negOrderIso.toHomeomorph
+#align ereal.neg_homeo EReal.negHomeo
+
+@[deprecated continuous_neg]
+protected theorem continuous_neg : Continuous fun x : EReal => -x :=
+  continuous_neg
+#align ereal.continuous_neg EReal.continuous_neg
+
+end EReal