mathlib documentation

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

source
@[instance]
def ereal.has_add  :
has_add ereal

source
@[instance]
def ereal.order_bot  :
order_bot ereal

source
@[instance]
def ereal.has_Sup  :
has_Sup ereal

source
@[instance]
def ereal.linear_order  :
linear_order ereal

source
@[instance]
def ereal.has_Inf  :
has_Inf ereal

source
@[instance]
def ereal.complete_lattice  :
complete_lattice ereal

source
@[instance]
def ereal.order_top  :
order_top ereal

source
def ereal  :
Type

ereal : The type [-∞, ∞]

Equations
source
@[instance]
def ereal.has_coe  :
has_coe ℝ ereal

Equations
source
@[simp]
theorem ereal.coe_real_le {x y : ℝ} :
↑x ≤ ↑y ↔ x ≤ y

source
@[simp]
theorem ereal.coe_real_lt {x y : ℝ} :
↑x < ↑y ↔ x < y

source
@[simp]
theorem ereal.coe_real_inj' {x y : ℝ} :
↑x = ↑y ↔ x = y

source
def ereal.neg (a : ereal) :
ereal

negation on ereal

Equations
source
@[instance]
def ereal.has_neg  :
has_neg ereal

Equations
source
theorem ereal.neg_def (x : ℝ) :
↑-x = -↑x

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

source
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

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

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

source
theorem ereal.neg_le {a b : ereal} :
-a ≤ b ↔ -b ≤ a

-a ≤ b ↔ -b ≤ a on ereal

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

a ≤ -b → b ≤ -a on ereal