mathlib3 documentation

topology.instances.ereal

Topological structure on ereal #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
noncomputable def ereal.topological_space  :
topological_space ereal
Equations
source
@[protected, instance]
def ereal.order_topology  :
order_topology ereal
source
@[protected, instance]
def ereal.t2_space  :
t2_space ereal
source
@[protected, instance]
def ereal.topological_space.second_countable_topology  :
topological_space.second_countable_topology ereal

Real coercion #

source
theorem ereal.embedding_coe  :
embedding coe
source
theorem ereal.open_embedding_coe  :
open_embedding coe
source
@[norm_cast]
theorem ereal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → ℝ} {a : ℝ} :
filter.tendsto (λ (a : α), ↑(m a)) f (nhds ↑a) ↔ filter.tendsto m f (nhds a)
source
theorem continuous_coe_real_ereal  :
continuous coe
source
theorem ereal.continuous_coe_iff {α : Type u_1} [topological_space α] {f : α → ℝ} :
continuous (λ (a : α), ↑(f a)) ↔ continuous f
source
theorem ereal.nhds_coe {r : ℝ} :
nhds ↑r = filter.map coe (nhds r)
source
theorem ereal.nhds_coe_coe {r p : ℝ} :
nhds (↑r, ↑p) = filter.map (λ (p : ℝ × ℝ), (↑(p.fst), ↑(p.snd))) (nhds (r, p))
source
theorem ereal.tendsto_to_real {a : ereal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
filter.tendsto ereal.to_real (nhds a) (nhds a.to_real)
source
theorem ereal.continuous_on_to_real  :
continuous_on ereal.to_real {⊥, ⊤}ᶜ
source
def ereal.ne_bot_top_homeomorph_real  :
↥{⊥, ⊤}ᶜ ≃ₜ ℝ

The set of finite ereal numbers is homeomorphic to ℝ.

Equations

ennreal coercion #

source
theorem ereal.embedding_coe_ennreal  :
embedding coe
source
@[norm_cast]
theorem ereal.tendsto_coe_ennreal {α : Type u_1} {f : filter α} {m : α → ennreal} {a : ennreal} :
filter.tendsto (λ (a : α), ↑(m a)) f (nhds ↑a) ↔ filter.tendsto m f (nhds a)
source
theorem continuous_coe_ennreal_ereal  :
continuous coe
source
theorem ereal.continuous_coe_ennreal_iff {α : Type u_1} [topological_space α] {f : α → ennreal} :
continuous (λ (a : α), ↑(f a)) ↔ continuous f

Neighborhoods of infinity #

source
theorem ereal.nhds_top  :
nhds ⊤ = ⨅ (a : ereal) (H : a ≠ ⊤), filter.principal (set.Ioi a)
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_1} {m : α → ereal} {f : filter α} :
filter.tendsto m f (nhds ⊤) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a
source
theorem ereal.nhds_bot  :
nhds ⊥ = ⨅ (a : ereal) (H : a ≠ ⊥), filter.principal (set.Iio a)
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_1} {m : α → ereal} {f : filter α} :
filter.tendsto m f (nhds ⊥) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x

Continuity of addition #

source
theorem ereal.continuous_at_add_coe_coe (a b : ℝ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (↑a, ↑b)
source
theorem ereal.continuous_at_add_top_coe (a : ℝ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (⊤, ↑a)
source
theorem ereal.continuous_at_add_coe_top (a : ℝ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (↑a, ⊤)
source
theorem ereal.continuous_at_add_top_top  :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (⊤, ⊤)
source
theorem ereal.continuous_at_add_bot_coe (a : ℝ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (⊥, ↑a)
source
theorem ereal.continuous_at_add_coe_bot (a : ℝ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (↑a, ⊥)
source
theorem ereal.continuous_at_add_bot_bot  :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (⊥, ⊥)
source
theorem ereal.continuous_at_add {p : ereal × ereal} (h : p.fst ≠ ⊤ ∨ p.snd ≠ ⊥) (h' : p.fst ≠ ⊥ ∨ p.snd ≠ ⊤) :
continuous_at (λ (p : ereal × ereal), 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
noncomputable def ereal.neg_homeo  :
ereal ≃ₜ ereal

Negation on ereal as a homeomorphism

Equations
source
theorem ereal.continuous_neg  :
continuous (λ (x : ereal), -x)