# mathlib3documentation

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 #

• 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 (nhds a) (nhds a)
theorem ereal.continuous_coe_iff {α : Type u_1} {f : α } :
continuous (λ (a : α), (f a))
theorem ereal.nhds_coe {r : } :
= (nhds r)
theorem ereal.nhds_coe_coe {r p : } :
nhds (r, p) = filter.map (λ (p : × ), ((p.fst), (p.snd))) (nhds (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 : α ennreal} {a : ennreal} :
filter.tendsto (λ (a : α), (m a)) f (nhds a) (nhds a)
theorem ereal.continuous_coe_ennreal_iff {α : Type u_1} {f : α ennreal} :
continuous (λ (a : α), (f a))

### Neighborhoods of infinity #

theorem ereal.nhds_top  :
= (a : ereal) (H : a ),
theorem ereal.nhds_top'  :
= (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 α} :
(nhds ) (x : ), ∀ᶠ (a : α) in f, x < m a
theorem ereal.nhds_bot  :
= (a : ereal) (H : a ),
theorem ereal.nhds_bot'  :
= (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 α} :
(nhds ) (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)