mathlib documentation

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

@[instance]

Real coercion #

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

The set of finite ereal numbers is homeomorphic to .

Equations

ennreal coercion #

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

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 : ), set.Ioi y s
theorem ereal.tendsto_nhds_top_iff_real {α : Type u_1} {m : α → ereal} {f : filter α} :
filter.tendsto m f (𝓝 ) ∀ (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 : ), set.Iio y s
theorem ereal.tendsto_nhds_bot_iff_real {α : Type u_1} {m : α → ereal} {f : filter α} :
filter.tendsto m f (𝓝 ) ∀ (x : ), ∀ᶠ (a : α) in f, m a < x

Continuity of addition #

theorem ereal.continuous_at_add_coe_coe (a b : ) :
continuous_at (λ (p : ereal × ereal), p.fst + p.snd) (a, b)
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 #

Negation on ereal as a homeomorphism

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