# Topological structure on EReal#

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

## Main results #

• Real.toEReal : ℝ → EReal is an open embedding
• ENNReal.toEReal : ℝ≥0∞ → EReal is a closed 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∞.

Equations
Equations
Equations
theorem EReal.denseRange_ratCast :
DenseRange fun (r : ) => r

### Real coercion #

theorem EReal.tendsto_coe {α : Type u_2} {f : } {m : α} {a : } :
Filter.Tendsto (fun (a : α) => (m a)) f (nhds a) Filter.Tendsto m f (nhds a)
theorem EReal.continuous_coe_iff {α : Type u_1} [] {f : α} :
(Continuous fun (a : α) => (f a))
theorem EReal.nhds_coe {r : } :
nhds r =
theorem EReal.nhds_coe_coe {r : } {p : } :
nhds (r, p) = Filter.map (fun (p : ) => (p.1, p.2)) (nhds (r, p))
theorem EReal.tendsto_toReal {a : EReal} (ha : a ) (h'a : a ) :

The set of finite EReal numbers is homeomorphic to ℝ.

Equations
Instances For

### ennreal coercion #

theorem EReal.tendsto_coe_ennreal {α : Type u_2} {f : } {m : αENNReal} {a : ENNReal} :
Filter.Tendsto (fun (a : α) => (m a)) f (nhds a) Filter.Tendsto m f (nhds a)
theorem EReal.continuous_coe_ennreal_iff {α : Type u_1} [] {f : αENNReal} :
(Continuous fun (a : α) => (f a))

### Neighborhoods of infinity #

theorem EReal.nhds_top :
= ⨅ (a : EReal), ⨅ (_ : a ),
theorem EReal.nhds_top_basis :
().HasBasis (fun (x : ) => True) fun (x : ) => Set.Ioi x
theorem EReal.nhds_top' :
= ⨅ (a : ),
theorem EReal.mem_nhds_top_iff {s : } :
s ∃ (y : ), Set.Ioi y s
theorem EReal.tendsto_nhds_top_iff_real {α : Type u_2} {m : αEReal} {f : } :
Filter.Tendsto m f () ∀ (x : ), ∀ᶠ (a : α) in f, x < m a
theorem EReal.nhds_bot :
= ⨅ (a : EReal), ⨅ (_ : a ),
theorem EReal.nhds_bot_basis :
().HasBasis (fun (x : ) => True) fun (x : ) => Set.Iio x
theorem EReal.nhds_bot' :
= ⨅ (a : ),
theorem EReal.mem_nhds_bot_iff {s : } :
s ∃ (y : ), Set.Iio y s
theorem EReal.tendsto_nhds_bot_iff_real {α : Type u_2} {m : αEReal} {f : } :
Filter.Tendsto m f () ∀ (x : ), ∀ᶠ (a : α) in f, m a < x

### Continuity of addition #

theorem EReal.continuousAt_add_coe_coe (a : ) (b : ) :
ContinuousAt (fun (p : ) => p.1 + p.2) (a, b)
theorem EReal.continuousAt_add_top_coe (a : ) :
ContinuousAt (fun (p : ) => p.1 + p.2) (, a)
theorem EReal.continuousAt_add_coe_top (a : ) :
ContinuousAt (fun (p : ) => p.1 + p.2) (a, )
ContinuousAt (fun (p : ) => p.1 + p.2) (, )
theorem EReal.continuousAt_add_bot_coe (a : ) :
ContinuousAt (fun (p : ) => p.1 + p.2) (, a)
theorem EReal.continuousAt_add_coe_bot (a : ) :
ContinuousAt (fun (p : ) => p.1 + p.2) (a, )
ContinuousAt (fun (p : ) => p.1 + p.2) (, )
theorem EReal.continuousAt_add {p : } (h : p.1 p.2 ) (h' : p.1 p.2 ) :
ContinuousAt (fun (p : ) => p.1 + p.2) p

The addition on EReal is continuous except where it doesn't make sense (i.e., at (⊥, ⊤) and at (⊤, ⊥)).

### Negation #

Equations
@[deprecated Homeomorph.neg]

Negation on EReal as a homeomorphism

Equations
Instances For
@[deprecated ContinuousNeg.continuous_neg]
theorem EReal.continuous_neg :
Continuous fun (x : EReal) => -x