Documentation

Mathlib.Topology.Instances.EReal.Lemmas

Topological structure on EReal #

We prove basic properties of the topology on EReal.

Main results #

Implementation #

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

Real coercion #

@[deprecated EReal.isEmbedding_coe (since := "2024-10-26")]

Alias of EReal.isEmbedding_coe.

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 #

      @[deprecated EReal.isEmbedding_coe_ennreal (since := "2024-10-26")]

      Alias of EReal.isEmbedding_coe_ennreal.

      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

      toENNReal #

      theorem Continuous.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : αEReal} (hf : Continuous f) :
      Continuous fun (x : α) => (f x).toENNReal
      @[deprecated Continuous.ereal_toENNReal (since := "2025-03-05")]
      theorem Continous.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : αEReal} (hf : Continuous f) :
      Continuous fun (x : α) => (f x).toENNReal

      Alias of Continuous.ereal_toENNReal.

      theorem ContinuousOn.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {s : Set α} {f : αEReal} (hf : ContinuousOn f s) :
      ContinuousOn (fun (x : α) => (f x).toENNReal) s
      theorem ContinuousWithinAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : αEReal} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) :
      ContinuousWithinAt (fun (x : α) => (f x).toENNReal) s x
      theorem ContinuousAt.ereal_toENNReal {α : Type u_2} [TopologicalSpace α] {f : αEReal} {x : α} (hf : ContinuousAt f x) :
      ContinuousAt (fun (x : α) => (f x).toENNReal) x

      Infs and Sups #

      theorem EReal.add_iInf_le_iInf_add {α : Type u_2} {u v : αEReal} :
      (⨅ (x : α), u x) + ⨅ (x : α), v x ⨅ (x : α), (u + v) x
      theorem EReal.iSup_add_le_add_iSup {α : Type u_2} {u v : αEReal} :
      ⨆ (x : α), (u + v) x (⨆ (x : α), u x) + ⨆ (x : α), v x

      Liminfs and Limsups #

      theorem EReal.liminf_neg {α : Type u_3} {f : Filter α} {v : αEReal} :
      theorem EReal.limsup_neg {α : Type u_3} {f : Filter α} {v : αEReal} :
      theorem EReal.le_liminf_add {α : Type u_3} {f : Filter α} {u v : αEReal} :
      theorem EReal.limsup_add_le {α : Type u_3} {f : Filter α} {u v : αEReal} (h : Filter.limsup u f Filter.limsup v f ) (h' : Filter.limsup u f Filter.limsup v f ) :
      theorem EReal.le_limsup_add {α : Type u_3} {f : Filter α} {u v : αEReal} :
      theorem EReal.liminf_add_le {α : Type u_3} {f : Filter α} {u v : αEReal} (h : Filter.limsup u f Filter.liminf v f ) (h' : Filter.limsup u f Filter.liminf v f ) :
      @[deprecated EReal.le_liminf_add (since := "2024-11-11")]
      theorem EReal.add_liminf_le_liminf_add {α : Type u_3} {f : Filter α} {u v : αEReal} :

      Alias of EReal.le_liminf_add.

      @[deprecated EReal.limsup_add_le (since := "2024-11-11")]

      Alias of EReal.limsup_add_le.

      @[deprecated EReal.le_limsup_add (since := "2024-11-11")]
      theorem EReal.limsup_add_liminf_le_limsup_add {α : Type u_3} {f : Filter α} {u v : αEReal} :

      Alias of EReal.le_limsup_add.

      @[deprecated EReal.liminf_add_le (since := "2024-11-11")]

      Alias of EReal.liminf_add_le.

      theorem EReal.limsup_add_bot_of_ne_top {α : Type u_3} {f : Filter α} {u v : αEReal} (h : Filter.limsup u f = ) (h' : Filter.limsup v f ) :
      theorem EReal.limsup_add_le_of_le {α : Type u_3} {f : Filter α} {u v : αEReal} {a b : EReal} (ha : Filter.limsup u f < a) (hb : Filter.limsup v f b) :
      Filter.limsup (u + v) f a + b
      theorem EReal.liminf_add_gt_of_gt {α : Type u_3} {f : Filter α} {u v : αEReal} {a 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_3} {f : Filter α} {u v : αEReal} (h : Filter.liminf u f = ) (h' : Filter.liminf v f ) :
      theorem EReal.le_limsup_mul {α : Type u_3} {f : Filter α} {u v : αEReal} (hu : ∃ᶠ (x : α) in f, 0 u x) (hv : 0 ≤ᶠ[f] v) :
      theorem EReal.limsup_mul_le {α : Type u_3} {f : Filter α} {u v : αEReal} (hu : ∃ᶠ (x : α) in f, 0 u x) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f 0 Filter.limsup v f ) (h₂ : Filter.limsup u f Filter.limsup v f 0) :
      theorem EReal.le_liminf_mul {α : Type u_3} {f : Filter α} {u v : αEReal} (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) :
      theorem EReal.liminf_mul_le {α : Type u_3} {f : Filter α} {u v : αEReal} [f.NeBot] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f 0 Filter.liminf v f ) (h₂ : Filter.limsup u f Filter.liminf v f 0) :

      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 (⊤, ⊥)).

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