data.real.ereal

# The extended reals [-∞, ∞].

This file defines ereal, the real numbers together with a top and bottom element, referred to as ⊤ and ⊥. It is implemented as with_top (with_bot ℝ)

Addition and multiplication are problematic in the presence of ±∞, but negation has a natural definition and satisfies the usual properties. An addition is derived, but ereal is not even a monoid (there is no identity).

ereal is a complete_lattice; this is now deduced by type class inference from the fact that with_top (with_bot L) is a complete lattice if L is a conditionally complete lattice.

## Tags

real, ereal, complete lattice

## TODO

abs : ereal → ennreal

In Isabelle they define + - * and / (making junk choices for things like -∞ + ∞) and then prove whatever bits of the ordered ring/field axioms still hold. They also do some limits stuff (liminf/limsup etc). See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

@[instance]

def ereal  :
Type

ereal : The type [-∞, ∞]

Equations
@[instance]

Equations
@[simp]
theorem ereal.coe_real_le {x y : } :
x y x y

@[simp]
theorem ereal.coe_real_lt {x y : } :
x < y x < y

@[simp]
theorem ereal.coe_real_inj' {x y : } :
x = y x = y

@[instance]

Equations
@[instance]

Equations

### Negation

def ereal.neg  :

negation on ereal

Equations
@[instance]

Equations
theorem ereal.neg_def (x : ) :

theorem ereal.neg_neg (a : ereal) :
--a = a
• -a = a on ereal
theorem ereal.neg_inj (a b : ereal) (h : -a = -b) :
a = b

theorem ereal.neg_eq_iff_neg_eq {a b : ereal} :
-a = b -b = a

Even though ereal is not an additive group, -a = b ↔ -b = a still holds

theorem ereal.neg_le_of_neg_le {a b : ereal} (h : -a b) :
-b a

if -a ≤ b then -b ≤ a on ereal

theorem ereal.neg_le {a b : ereal} :
-a b -b a

-a ≤ b ↔ -b ≤ a on ereal

theorem ereal.le_neg_of_le_neg {a b : ereal} (h : a -b) :
b -a

a ≤ -b → b ≤ -a on ereal