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 #

Implementation #

Most proofs are adapted from the corresponding proofs on ℝ≥0∞.

source
instance EReal.instTopologicalSpaceEReal :
TopologicalSpace EReal
Equations
source
instance EReal.instOrderTopologyERealInstTopologicalSpaceERealToPreorderInstERealPartialOrder :
OrderTopology EReal
Equations
source
instance EReal.instT5SpaceERealInstTopologicalSpaceEReal :
T5Space EReal
Equations
source
instance EReal.instT2SpaceERealInstTopologicalSpaceEReal :
T2Space EReal
Equations
source
theorem EReal.denseRange_ratCast :
DenseRange fun r => ↑↑r
source
instance EReal.instSecondCountableTopologyERealInstTopologicalSpaceEReal :
TopologicalSpace.SecondCountableTopology EReal
Equations

Real coercion #

source
theorem EReal.embedding_coe :
Embedding Real.toEReal
source
theorem EReal.openEmbedding_coe :
OpenEmbedding 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.fst, ↑p.snd)) (nhds (r, p))
source
theorem EReal.tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
Filter.Tendsto EReal.toReal (nhds a) (nhds (EReal.toReal a))
source
theorem EReal.continuousOn_toReal :
ContinuousOn EReal.toReal {⊥, ⊤}ᶜ
source
def EReal.neBotTopHomeomorphReal :
↑{⊥, ⊤}ᶜ ≃ₜ ℝ

The set of finite EReal numbers is homeomorphic to ℝ.

Equations
Instances For

    ennreal coercion #

    source
    theorem EReal.embedding_coe_ennreal :
    Embedding ENNReal.toEReal
    source
    theorem EReal.closedEmbedding_coe_ennreal :
    ClosedEmbedding 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 :
    Filter.HasBasis (nhds ⊤) (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 :
    Filter.HasBasis (nhds ⊥) (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

    Continuity of addition #

    source
    theorem EReal.continuousAt_add_coe_coe (a : ℝ) (b : ℝ) :
    ContinuousAt (fun p => p.fst + p.snd) (↑a, ↑b)
    source
    theorem EReal.continuousAt_add_top_coe (a : ℝ) :
    ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a)
    source
    theorem EReal.continuousAt_add_coe_top (a : ℝ) :
    ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊤)
    source
    theorem EReal.continuousAt_add_top_top :
    ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
    source
    theorem EReal.continuousAt_add_bot_coe (a : ℝ) :
    ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a)
    source
    theorem EReal.continuousAt_add_coe_bot (a : ℝ) :
    ContinuousAt (fun p => p.fst + p.snd) (↑a, ⊥)
    source
    theorem EReal.continuousAt_add_bot_bot :
    ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
    source
    theorem EReal.continuousAt_add {p : EReal × EReal} (h : p.fst ≠ ⊤ ∨ p.snd ≠ ⊥) (h' : p.fst ≠ ⊥ ∨ p.snd ≠ ⊤) :
    ContinuousAt (fun p => p.fst + p.snd) p

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

    Negation #

    source
    instance EReal.instContinuousNegERealInstTopologicalSpaceERealInstNegEReal :
    ContinuousNeg EReal
    Equations
    source
    @[deprecated Homeomorph.neg]
    def EReal.negHomeo :
    EReal ≃ₜ EReal

    Negation on EReal as a homeomorphism

    Equations
    Instances For
      source
      @[deprecated ContinuousNeg.continuous_neg]
      theorem EReal.continuous_neg :
      Continuous fun x => -x