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

instance EReal.instTopologicalSpace : TopologicalSpace EReal

Equations

• EReal.instTopologicalSpace = Preorder.topology EReal

instance EReal.instOrderTopology : OrderTopology EReal

Equations

• EReal.instOrderTopology = ⋯

instance EReal.instT5Space : T5Space EReal

Equations

• EReal.instT5Space = ⋯

instance EReal.instT2Space : T2Space EReal

Equations

• EReal.instT2Space = ⋯

theorem EReal.denseRange_ratCast : DenseRange fun (r : ℚ) => ↑↑r

instance EReal.instSecondCountableTopology : SecondCountableTopology EReal

Equations

• EReal.instSecondCountableTopology = ⋯

Real coercion

theorem EReal.embedding_coe : Embedding Real.toEReal

theorem EReal.openEmbedding_coe : OpenEmbedding Real.toEReal

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)

theorem continuous_coe_real_ereal : Continuous Real.toEReal

theorem EReal.continuous_coe_iff {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

theorem EReal.nhds_coe {r : ℝ} : nhds ↑r = Filter.map Real.toEReal (nhds r)

theorem EReal.nhds_coe_coe {r : ℝ} {p : ℝ} : nhds (↑r, ↑p) = Filter.map (fun (p : ℝ × ℝ) => (↑p.1, ↑p.2)) (nhds (r, p))

theorem EReal.tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) : Filter.Tendsto EReal.toReal (nhds a) (nhds a.toReal)

theorem EReal.continuousOn_toReal : ContinuousOn EReal.toReal {⊥, ⊤}ᶜ

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 }

ENNReal coercion

theorem EReal.embedding_coe_ennreal : Embedding ENNReal.toEReal

theorem EReal.closedEmbedding_coe_ennreal : ClosedEmbedding ENNReal.toEReal

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)

theorem continuous_coe_ennreal_ereal : Continuous ENNReal.toEReal

theorem EReal.continuous_coe_ennreal_iff {α : Type u_1} [TopologicalSpace α] {f : α → ENNReal} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

Neighborhoods of infinity

theorem EReal.nhds_top : nhds ⊤ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)

theorem EReal.nhds_top_basis : (nhds ⊤).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Ioi ↑x

theorem EReal.nhds_top' : nhds ⊤ = ⨅ (a : ℝ), Filter.principal (Set.Ioi ↑a)

theorem EReal.mem_nhds_top_iff {s : Set EReal} : s ∈ nhds ⊤ ↔ ∃ (y : ℝ), Set.Ioi ↑y ⊆ s

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

theorem EReal.nhds_bot : nhds ⊥ = ⨅ (a : EReal), ⨅ (_ : a ≠ ⊥), Filter.principal (Set.Iio a)

theorem EReal.nhds_bot_basis : (nhds ⊥).HasBasis (fun (x : ℝ) => True) fun (x : ℝ) => Set.Iio ↑x

theorem EReal.nhds_bot' : nhds ⊥ = ⨅ (a : ℝ), Filter.principal (Set.Iio ↑a)

theorem EReal.mem_nhds_bot_iff {s : Set EReal} : s ∈ nhds ⊥ ↔ ∃ (y : ℝ), Set.Iio ↑y ⊆ s

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

theorem EReal.nhdsWithin_top : nhdsWithin ⊤ {⊤}ᶜ = Filter.map Real.toEReal Filter.atTop

theorem EReal.nhdsWithin_bot : nhdsWithin ⊥ {⊥}ᶜ = Filter.map Real.toEReal Filter.atBot

theorem EReal.tendsto_toReal_atTop : Filter.Tendsto EReal.toReal (nhdsWithin ⊤ {⊤}ᶜ) Filter.atTop

theorem EReal.tendsto_toReal_atBot : Filter.Tendsto EReal.toReal (nhdsWithin ⊥ {⊥}ᶜ) Filter.atBot

Infs and Sups

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

theorem EReal.iSup_add_le_add_iSup {α : Type u_2} {u : α → EReal} {v : α → EReal} (h : ⨆ (x : α), u x ≠ ⊥ ∨ ⨆ (x : α), v x ≠ ⊤) (h' : ⨆ (x : α), u x ≠ ⊤ ∨ ⨆ (x : α), v x ≠ ⊥) : ⨆ (x : α), (u + v) x ≤ (⨆ (x : α), u x) + ⨆ (x : α), v x

Liminfs and Limsups

theorem EReal.liminf_neg {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.liminf (-v) f = -Filter.limsup v f

theorem EReal.limsup_neg {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.limsup (-v) f = -Filter.liminf v f

theorem EReal.add_liminf_le_liminf_add {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} : Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f

theorem EReal.limsup_add_le_add_limsup {α : Type u_3} {f : Filter α} {u : α → EReal} {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

theorem EReal.limsup_add_liminf_le_limsup_add {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} : Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f

theorem EReal.liminf_add_le_limsup_add_liminf {α : Type u_3} {f : Filter α} {u : α → EReal} {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

theorem EReal.limsup_add_bot_of_ne_top {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} (h : Filter.limsup u f = ⊥) (h' : Filter.limsup v f ≠ ⊤) : Filter.limsup (u + v) f = ⊥

theorem EReal.limsup_add_le_of_le {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} {a : EReal} {b : EReal} (ha : Filter.limsup u f < a) (hb : Filter.limsup v f ≤ b) : Filter.limsup (u + v) f ≤ a + b

theorem EReal.liminf_add_gt_of_gt {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} {a : EReal} {b : EReal} (ha : a < Filter.liminf u f) (hb : b < Filter.liminf v f) : a + b < Filter.liminf (u + v) f

theorem EReal.liminf_add_top_of_ne_bot {α : Type u_3} {f : Filter α} {u : α → EReal} {v : α → EReal} (h : Filter.liminf u f = ⊤) (h' : Filter.liminf v f ≠ ⊥) : Filter.liminf (u + v) f = ⊤

theorem EReal.limsup_le_iff {α : Type u_3} {f : Filter α} {u : α → EReal} {b : EReal} : Filter.limsup u f ≤ b ↔ ∀ (c : ℝ), b < ↑c → ∀ᶠ (a : α) in f, u a ≤ ↑c

Continuity of addition

theorem EReal.continuousAt_add_coe_coe (a : ℝ) (b : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ↑b)

theorem EReal.continuousAt_add_top_coe (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ↑a)

theorem EReal.continuousAt_add_coe_top (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊤)

theorem EReal.continuousAt_add_top_top : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊤, ⊤)

theorem EReal.continuousAt_add_bot_coe (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ↑a)

theorem EReal.continuousAt_add_coe_bot (a : ℝ) : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (↑a, ⊥)

theorem EReal.continuousAt_add_bot_bot : ContinuousAt (fun (p : EReal × EReal) => p.1 + p.2) (⊥, ⊥)

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 (⊤, ⊥)).

Negation

instance EReal.instContinuousNeg : ContinuousNeg EReal

Equations

• EReal.instContinuousNeg = ⋯

Continuity of multiplication

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).