@[instance]
Equations
- ennreal.inhabited = {default := 0}
@[instance]
Equations
to_nnreal x returns x if it is real, otherwise 0.
Equations
of_real x returns x if it is nonnegative, 0 otherwise.
Equations
- ennreal.of_real r = ↑(nnreal.of_real r)
@[simp]
Coercion ℝ≥0 → ennreal as a ring_hom.
Equations
- ennreal.of_nnreal_hom = {to_fun := coe coe_to_lift, map_one' := ennreal.coe_one, map_mul' := ennreal.of_nnreal_hom._proof_1, map_zero' := ennreal.coe_zero, map_add' := ennreal.of_nnreal_hom._proof_2}
theorem
ennreal.lt_iff_exists_real_btwn
{a b : ennreal} :
a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ennreal.of_real r ∧ ennreal.of_real r < b
theorem
ennreal.coe_mem_upper_bounds
{r : nnreal}
{s : set nnreal} :
↑r ∈ upper_bounds (coe '' s) ↔ r ∈ upper_bounds s
@[instance]
Equations
- ennreal.has_sub = {sub := λ (a b : ennreal), has_Inf.Inf {d : ennreal | a ≤ d + b}}
@[instance]
Equations
- ennreal.has_inv = {inv := λ (a : ennreal), has_Inf.Inf {b : ennreal | 1 ≤ a * b}}
theorem
ennreal.of_real_add
{p q : ℝ} :
0 ≤ p → 0 ≤ q → ennreal.of_real (p + q) = ennreal.of_real p + ennreal.of_real q
theorem
ennreal.of_real_add_le
{p q : ℝ} :
ennreal.of_real (p + q) ≤ ennreal.of_real p + ennreal.of_real q
@[simp]
theorem
ennreal.of_real_le_of_real_iff
{p q : ℝ} :
0 ≤ q → (ennreal.of_real p ≤ ennreal.of_real q ↔ p ≤ q)
@[simp]
theorem
ennreal.of_real_lt_of_real_iff
{p q : ℝ} :
0 < q → (ennreal.of_real p < ennreal.of_real q ↔ p < q)
theorem
ennreal.of_real_lt_of_real_iff_of_nonneg
{p q : ℝ} :
0 ≤ p → (ennreal.of_real p < ennreal.of_real q ↔ p < q)
theorem
ennreal.to_real_le_of_le_of_real
{a : ennreal}
{b : ℝ} :
0 ≤ b → a ≤ ennreal.of_real b → a.to_real ≤ b
theorem
ennreal.of_real_mul
{p q : ℝ} :
0 ≤ p → ennreal.of_real (p * q) = ennreal.of_real p * ennreal.of_real q
supr_mul, mul_supr and variants are in topology.instances.ennreal.