Documentation

Mathlib.Topology.Instances.EReal

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 :

Equations

EReal.instT5Space = ⋯

instance EReal.instT2Space :

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 }

Instances For

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

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 = ⋯