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

    Liminfs and Limsups #

    theorem EReal.liminf_le_liminf {α : Type u_2} {f : Filter α} {u : αEReal} {v : αEReal} (h : u ≤ᶠ[f] v) :
    theorem EReal.limsup_le_limsup {α : Type u_2} {f : Filter α} {u : αEReal} {v : αEReal} (h : u ≤ᶠ[f] v) :
    theorem EReal.limsup_add_lt_of_lt {α : Type u_2} {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.limsup_add_bot_of_ne_top {α : Type u_2} {f : Filter α} {u : αEReal} {v : αEReal} (h : Filter.limsup u f = ) (h' : Filter.limsup v f ) :
    theorem EReal.limsup_add_le_add_limsup {α : Type u_2} {f : Filter α} {u : αEReal} {v : αEReal} (h : Filter.limsup u f Filter.limsup v f ) (h' : Filter.limsup u f Filter.limsup v f ) :
    theorem EReal.limsup_add_le_of_le {α : Type u_2} {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_neg {α : Type u_2} {f : Filter α} {v : αEReal} :
    theorem EReal.limsup_neg {α : Type u_2} {f : Filter α} {v : αEReal} :
    theorem EReal.liminf_add_gt_of_gt {α : Type u_2} {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_2} {f : Filter α} {u : αEReal} {v : αEReal} (h : Filter.liminf u f = ) (h' : Filter.liminf v f ) :
    theorem EReal.add_liminf_le_liminf_add {α : Type u_2} {f : Filter α} {u : αEReal} {v : αEReal} :
    theorem EReal.limsup_le_iff {α : Type u_2} {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_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 #

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