# Topological structure on `EReal` #

We prove basic properties of the topology on `EReal`.

## 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∞`.

### Real coercion #

source
theorem EReal.isEmbedding_coe :
Topology.IsEmbedding Real.toEReal
source
theorem EReal.isOpenEmbedding_coe :
Topology.IsOpenEmbedding Real.toEReal
source
theorem EReal.tendsto_coe {α : Type u_2} {f : Filter α} {m : α → ℝ} {a : ℝ} :
Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)
source
theorem continuous_coe_real_ereal :
Continuous Real.toEReal
source
theorem EReal.continuous_coe_iff {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} :
(Continuous fun (a : α) => ↑(f a)) ↔ Continuous f
source
theorem EReal.nhds_coe {r : ℝ} :
nhds ↑r = Filter.map Real.toEReal (nhds r)
source
theorem EReal.nhds_coe_coe {r p : ℝ} :
nhds (↑r, ↑p) = Filter.map (fun (p : ℝ × ℝ) => (↑p.1, ↑p.2)) (nhds (r, p))
source
theorem EReal.tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
Filter.Tendsto toReal (nhds a) (nhds a.toReal)
source
theorem EReal.continuousOn_toReal :
ContinuousOn toReal {⊥, ⊤}ᶜ
source
def EReal.neBotTopHomeomorphReal :
↑{⊥, ⊤}ᶜ ≃ₜ ℝ

The set of finite `EReal` numbers is homeomorphic to `ℝ`.

Equations

- EReal.neBotTopHomeomorphReal = { toEquiv := EReal.neTopBotEquivReal, continuous_toFun := EReal.neBotTopHomeomorphReal._proof_1, continuous_invFun := EReal.neBotTopHomeomorphReal._proof_2 }

Instances For

### ENNReal coercion #

source
theorem EReal.isEmbedding_coe_ennreal :
Topology.IsEmbedding ENNReal.toEReal
source
theorem EReal.isClosedEmbedding_coe_ennreal :
Topology.IsClosedEmbedding ENNReal.toEReal
source
theorem EReal.tendsto_coe_ennreal {α : Type u_2} {f : Filter α} {m : α → ENNReal} {a : ENNReal} :
Filter.Tendsto (fun (a : α) => ↑(m a)) f (nhds ↑a) ↔ Filter.Tendsto m f (nhds a)
source
theorem continuous_coe_ennreal_ereal :
Continuous ENNReal.toEReal
source
theorem EReal.continuous_coe_ennreal_iff {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} :
(Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

### Neighborhoods of infinity #

source
theorem EReal.nhds_top :
nhds ⊤ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)
source
theorem EReal.nhds_top_basis :
(nhds ⊤).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Ioi ↑x
source
theorem EReal.nhds_top' :
nhds ⊤ = ⨅ (a : ℝ), Filter.principal (Set.Ioi ↑a)
source
theorem EReal.mem_nhds_top_iff {s : Set EReal} :
s ∈ nhds ⊤ ↔ ∃ (y : ℝ), Set.Ioi ↑y ⊆ s
source
theorem EReal.tendsto_nhds_top_iff_real {α : Type u_2} {m : α → EReal} {f : Filter α} :
Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
source
theorem EReal.nhds_bot :
nhds ⊥ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊥), Filter.principal (Set.Iio a)
source
theorem EReal.nhds_bot_basis :
(nhds ⊥).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Iio ↑x
source
theorem EReal.nhds_bot' :
nhds ⊥ = ⨅ (a : ℝ), Filter.principal (Set.Iio ↑a)
source
theorem EReal.mem_nhds_bot_iff {s : Set EReal} :
s ∈ nhds ⊥ ↔ ∃ (y : ℝ), Set.Iio ↑y ⊆ s
source
theorem EReal.tendsto_nhds_bot_iff_real {α : Type u_2} {m : α → EReal} {f : Filter α} :
Filter.Tendsto m f (nhds ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x
source
theorem EReal.nhdsWithin_top :
nhdsWithin ⊤ {⊤}ᶜ = Filter.map Real.toEReal Filter.atTop
source
theorem EReal.nhdsWithin_bot :
nhdsWithin ⊥ {⊥}ᶜ = Filter.map Real.toEReal Filter.atBot
source
@[simp]
theorem EReal.tendsto_coe_nhds_top_iff {α : Type u_1} {f : α → ℝ} {l : Filter α} :
Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop
source
theorem EReal.tendsto_coe_atTop :
Filter.Tendsto Real.toEReal Filter.atTop (nhds ⊤)
source
@[simp]
theorem EReal.tendsto_coe_nhds_bot_iff {α : Type u_1} {f : α → ℝ} {l : Filter α} :
Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊥) ↔ Filter.Tendsto f l Filter.atBot
source
theorem EReal.tendsto_coe_atBot :
Filter.Tendsto Real.toEReal Filter.atBot (nhds ⊥)
source
theorem EReal.tendsto_toReal_atTop :
Filter.Tendsto toReal (nhdsWithin ⊤ {⊤}ᶜ) Filter.atTop
source
theorem EReal.tendsto_toReal_atBot :
Filter.Tendsto toReal (nhdsWithin ⊥ {⊥}ᶜ) Filter.atBot

### toENNReal #

source
theorem EReal.continuous_toENNReal :
Continuous toENNReal
source
theorem Continuous.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} (hf : Continuous f) :
Continuous fun (x : α) => (f x).toENNReal
source
theorem ContinuousOn.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {s : Set α} {f : α → EReal} (hf : ContinuousOn f s) :
ContinuousOn (fun (x : α) => (f x).toENNReal) s
source
theorem ContinuousWithinAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
ContinuousWithinAt (fun (x : α) => (f x).toENNReal) s x
source
theorem ContinuousAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : α → EReal} {x : α} (hf : ContinuousAt f x) :
ContinuousAt (fun (x : α) => (f x).toENNReal) x

### Infs and Sups #

source
theorem EReal.add_iInf_le_iInf_add {α : Type u_2} {u v : α → EReal} :
(⨅ (x : α), u x) + ⨅ (x : α), v x ≤ ⨅ (x : α), (u + v) x
source
theorem EReal.iSup_add_le_add_iSup {α : Type u_2} {u v : α → EReal} :
⨆ (x : α), (u + v) x ≤ (⨆ (x : α), u x) + ⨆ (x : α), v x

### Liminfs and Limsups #

source
theorem EReal.liminf_neg {α : Type u_3} {f : Filter α} {v : α → EReal} :
Filter.liminf (-v) f = -Filter.limsup v f
source
theorem EReal.limsup_neg {α : Type u_3} {f : Filter α} {v : α → EReal} :
Filter.limsup (-v) f = -Filter.liminf v f
source
theorem EReal.le_liminf_add {α : Type u_3} {f : Filter α} {u v : α → EReal} :
Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
source
theorem EReal.limsup_add_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.limsup v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ ⊥) :
Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
source
theorem EReal.le_limsup_add {α : Type u_3} {f : Filter α} {u v : α → EReal} :
Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
source
theorem EReal.liminf_add_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.liminf v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ ⊥) :
Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
source
theorem EReal.limsup_add_bot_of_ne_top {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f = ⊥) (h' : Filter.limsup v f ≠ ⊤) :
Filter.limsup (u + v) f = ⊥
source
theorem EReal.limsup_add_le_of_le {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : Filter.limsup u f < a) (hb : Filter.limsup v f ≤ b) :
Filter.limsup (u + v) f ≤ a + b
source
theorem EReal.liminf_add_gt_of_gt {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : a < Filter.liminf u f) (hb : b < Filter.liminf v f) :
a + b < Filter.liminf (u + v) f
source
theorem EReal.liminf_add_top_of_ne_bot {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.liminf u f = ⊤) (h' : Filter.liminf v f ≠ ⊥) :
Filter.liminf (u + v) f = ⊤
source
theorem EReal.le_limsup_mul {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) :
Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
source
theorem EReal.limsup_mul_le {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) :
Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
source
theorem EReal.le_liminf_mul {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) :
Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
source
theorem EReal.liminf_mul_le {α : Type u_3} {f : Filter α} {u v : α → EReal} [f.NeBot] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) :
Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f

### Continuity of addition #

source
theorem EReal.continuousAt_add_coe_coe (a b : ℝ) :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ↑b)
source
theorem EReal.continuousAt_add_top_coe (a : ℝ) :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ↑a)
source
theorem EReal.continuousAt_add_coe_top (a : ℝ) :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊤)
source
theorem EReal.continuousAt_add_top_top :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ⊤)
source
theorem EReal.continuousAt_add_bot_coe (a : ℝ) :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ↑a)
source
theorem EReal.continuousAt_add_coe_bot (a : ℝ) :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊥)
source
theorem EReal.continuousAt_add_bot_bot :
ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ⊥)
source
theorem EReal.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

The addition on `EReal` is continuous except where it doesn't make sense (i.e., at `(⊥, ⊤)` and at `(⊤, ⊥)`).

source
theorem EReal.lowerSemicontinuous_add :
LowerSemicontinuous fun (p : EReal × EReal) => p.1 + p.2

### Continuity of multiplication #

source
theorem EReal.continuousAt_mul {p : EReal × EReal} (h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥) (h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤) (h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0) (h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0) :
ContinuousAt (fun (p : EReal × EReal) => p.1 * p.2) p

The multiplication on `EReal` is continuous except at indeterminacies (i.e. whenever one value is zero and the other infinite).

source
theorem EReal.tendsto_mul {a b : EReal} (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) (h₃ : a ≠ ⊥ ∨ b ≠ 0) (h₄ : a ≠ ⊤ ∨ b ≠ 0) :
Filter.Tendsto (fun (p : EReal × EReal) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))
source
theorem EReal.Tendsto.mul {α : Type u_2} {f : Filter α} {ma mb : α → EReal} {a b : EReal} (hma : Filter.Tendsto ma f (nhds a)) (hmb : Filter.Tendsto mb f (nhds b)) (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) (h₃ : a ≠ ⊥ ∨ b ≠ 0) (h₄ : a ≠ ⊤ ∨ b ≠ 0) :
Filter.Tendsto (fun (x : α) => ma x * mb x) f (nhds (a * b))
source
theorem EReal.Tendsto.const_mul {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Filter.Tendsto m f (nhds b)) (h₁ : a ≠ ⊥ ∨ b ≠ 0) (h₂ : a ≠ ⊤ ∨ b ≠ 0) :
Filter.Tendsto (fun (b : α) => a * m b) f (nhds (a * b))
source
theorem EReal.Tendsto.mul_const {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal} (hm : Filter.Tendsto m f (nhds a)) (h₁ : a ≠ 0 ∨ b ≠ ⊥) (h₂ : a ≠ 0 ∨ b ≠ ⊤) :
Filter.Tendsto (fun (x : α) => m x * b) f (nhds (a * b))