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.instTopologicalSpaceEReal : TopologicalSpace EReal

Equations

• EReal.instTopologicalSpaceEReal = Preorder.topology EReal

instance EReal.instOrderTopologyERealInstTopologicalSpaceERealToPreorderInstERealPartialOrder : OrderTopology EReal

Equations

• EReal.instOrderTopologyERealInstTopologicalSpaceERealToPreorderInstERealPartialOrder = ⋯

instance EReal.instT5SpaceERealInstTopologicalSpaceEReal : T5Space EReal

Equations

• EReal.instT5SpaceERealInstTopologicalSpaceEReal = ⋯

instance EReal.instT2SpaceERealInstTopologicalSpaceEReal : T2Space EReal

Equations

• EReal.instT2SpaceERealInstTopologicalSpaceEReal = ⋯

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

instance EReal.instSecondCountableTopologyERealInstTopologicalSpaceEReal : SecondCountableTopology EReal

Equations

• EReal.instSecondCountableTopologyERealInstTopologicalSpaceEReal = ⋯

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 (EReal.toReal a))

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 : Filter.HasBasis (nhds ⊤) (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 : Filter.HasBasis (nhds ⊥) (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.instContinuousNegERealInstTopologicalSpaceERealInstNegEReal : ContinuousNeg EReal

Equations

• EReal.instContinuousNegERealInstTopologicalSpaceERealInstNegEReal = ⋯

@[deprecated Homeomorph.neg]

def EReal.negHomeo : EReal ≃ₜ EReal

Negation on EReal as a homeomorphism

Equations

• EReal.negHomeo = OrderIso.toHomeomorph EReal.negOrderIso

@[deprecated ContinuousNeg.continuous_neg]

theorem EReal.continuous_neg : Continuous fun (x : EReal) => -x