mathlibdocumentation

topology.instances.ereal

Topological structure on ereal#

We endow ereal with the order topology, and prove basic properties of this topology.

Main results #

• coe : ℝ → ereal is an open embedding
• coe : ℝ≥0∞ → ereal is an embedding
• The addition on ereal is continuous except at (⊥, ⊤) and at (⊤, ⊥).
• Negation is a homeomorphism on ereal.

Implementation #

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

@[protected, instance]
noncomputable def ereal.topological_space  :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]

Real coercion #

@[norm_cast]
theorem ereal.tendsto_coe {α : Type u_1} {f : filter α} {m : α → } {a : } :
filter.tendsto (λ (a : α), (m a)) f (𝓝 a) (𝓝 a)
theorem ereal.continuous_coe_iff {α : Type u_1} {f : α → } :
continuous (λ (a : α), (f a))
theorem ereal.nhds_coe {r : } :
𝓝 r = (𝓝 r)
theorem ereal.nhds_coe_coe {r p : } :
𝓝 (r, p) = filter.map (λ (p : × ), ((p.fst), (p.snd))) (𝓝 (r, p))
theorem ereal.tendsto_to_real {a : ereal} (ha : a ) (h'a : a ) :

The set of finite ereal numbers is homeomorphic to .

Equations

ennreal coercion #

@[norm_cast]
theorem ereal.tendsto_coe_ennreal {α : Type u_1} {f : filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
filter.tendsto (λ (a : α), (m a)) f (𝓝 a) (𝓝 a)
theorem ereal.continuous_coe_ennreal_iff {α : Type u_1} {f : α → ℝ≥0∞} :
continuous (λ (a : α), (f a))

Neighborhoods of infinity #

theorem ereal.nhds_top  :
= ⨅ (a : ereal) (H : a ), 𝓟 (set.Ioi a)
theorem ereal.nhds_top'  :
= ⨅ (a : ), 𝓟 (set.Ioi a)
theorem ereal.mem_nhds_top_iff {s : set ereal} :
s ∃ (y : ), s
theorem ereal.tendsto_nhds_top_iff_real {α : Type u_1} {m : α → ereal} {f : filter α} :
(𝓝 ) ∀ (x : ), ∀ᶠ (a : α) in f, x < m a
theorem ereal.nhds_bot  :
= ⨅ (a : ereal) (H : a ), 𝓟 (set.Iio a)
theorem ereal.nhds_bot'  :
= ⨅ (a : ), 𝓟 (set.Iio a)
theorem ereal.mem_nhds_bot_iff {s : set ereal} :
s ∃ (y : ), s
theorem ereal.tendsto_nhds_bot_iff_real {α : Type u_1} {m : α → ereal} {f : filter α} :
(𝓝 ) ∀ (x : ), ∀ᶠ (a : α) in f, m a < x

theorem ereal.continuous_at_add_coe_coe (a b : ) :
continuous_at (λ (p : , p.fst + p.snd) (a, b)
theorem ereal.continuous_at_add_top_coe (a : ) :
continuous_at (λ (p : , p.fst + p.snd) (, a)
theorem ereal.continuous_at_add_coe_top (a : ) :
continuous_at (λ (p : , p.fst + p.snd) (a, )
theorem ereal.continuous_at_add_bot_coe (a : ) :
continuous_at (λ (p : , p.fst + p.snd) (, a)
theorem ereal.continuous_at_add_coe_bot (a : ) :
continuous_at (λ (p : , p.fst + p.snd) (a, )
theorem ereal.continuous_at_add {p : ereal × ereal} (h : p.fst p.snd ) (h' : p.fst p.snd ) :
continuous_at (λ (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 #

noncomputable def ereal.neg_homeo  :

Negation on ereal as a homeomorphism

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