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

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

Real coercion #

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 EReal.continuous_coe_iff {α : Type u_1} [TopologicalSpace α] {f : α} :
(Continuous fun (a : α) => (f a)) Continuous f
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 ) :

The set of finite EReal numbers is homeomorphic to .

Equations
Instances For

    ennreal coercion #

    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 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.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.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_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 {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 #