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

@[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 (nhds a) filter.tendsto m f (nhds 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 : } :
nhds (r, p) = filter.map (λ (p : × ), ((p.fst), (p.snd))) (nhds (r, p))

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 : α ennreal} {a : ennreal} :
filter.tendsto (λ (a : α), (m a)) f (nhds a) filter.tendsto m f (nhds a)
theorem ereal.continuous_coe_ennreal_iff {α : Type u_1} [topological_space α] {f : α ennreal} :
continuous (λ (a : α), (f a)) continuous f

Neighborhoods of infinity #

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
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 #

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 #

noncomputable def ereal.neg_homeo  :

Negation on ereal as a homeomorphism

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