Extended non-negative reals

We define ENNReal = ℝ≥0∞ := WithTop ℝ≥0 to be the type of extended nonnegative real numbers, i.e., the interval [0, +∞]. This type is used as the codomain of a MeasureTheory.Measure, and of the extended distance edist in an EMetricSpace.

In this file we set up many of the instances on ℝ≥0∞, and provide relationships between ℝ≥0∞ and ℝ≥0, and between ℝ≥0∞ and ℝ. In particular, we provide a coercion from ℝ≥0 to ℝ≥0∞ as well as functions ENNReal.toNNReal, ENNReal.ofReal and ENNReal.toReal, all of which take the value zero wherever they cannot be the identity. Also included is the relationship between ℝ≥0∞ and ℕ. The interaction of these functions, especially ENNReal.ofReal and ENNReal.toReal, with the algebraic and lattice structure can be found in Data.ENNReal.Real.

This file proves many of the order properties of ℝ≥0∞, with the exception of the ways those relate to the algebraic structure, which are included in Data.ENNReal.Operations. This file also defines inversion and division: this includes Inv and Div instances on ℝ≥0∞ making it into a DivInvOneMonoid. As a consequence of being a DivInvOneMonoid, ℝ≥0∞ inherits a power operation with integer exponent: this and other properties is shown in Data.ENNReal.Inv.

Main definitions

• ℝ≥0∞: the extended nonnegative real numbers [0, ∞]; defined as WithTop ℝ≥0; it is equipped with the following structures:

  • coercion from ℝ≥0 defined in the natural way;

  • the natural structure of a complete dense linear order: ↑p ≤ ↑q ↔ p ≤ q and ∀ a, a ≤ ∞;

  • a + b is defined so that ↑p + ↑q = ↑(p + q) for (p q : ℝ≥0) and a + ∞ = ∞ + a = ∞;

  • a * b is defined so that ↑p * ↑q = ↑(p * q) for (p q : ℝ≥0), 0 * ∞ = ∞ * 0 = 0, and a * ∞ = ∞ * a = ∞ for a ≠ 0;

  • a - b is defined as the minimal d such that a ≤ d + b; this way we have ↑p - ↑q = ↑(p - q), ∞ - ↑p = ∞, ↑p - ∞ = ∞ - ∞ = 0; note that there is no negation, only subtraction;

  The addition and multiplication defined this way together with 0 = ↑0 and 1 = ↑1 turn ℝ≥0∞ into a canonically ordered commutative semiring of characteristic zero.

  • a⁻¹ is defined as Inf {b | 1 ≤ a * b}. This way we have (↑p)⁻¹ = ↑(p⁻¹) for p : ℝ≥0, p ≠ 0, 0⁻¹ = ∞, and ∞⁻¹ = 0.
  • a / b is defined as a * b⁻¹.

  This inversion and division include Inv and Div instances on ℝ≥0∞, making it into a DivInvOneMonoid. Further properties of these are shown in Data.ENNReal.Inv.

• Coercions to/from other types:

  • coercion ℝ≥0 → ℝ≥0∞ is defined as Coe, so one can use (p : ℝ≥0) in a context that expects a : ℝ≥0∞, and Lean will apply coe automatically;

  • ENNReal.toNNReal sends ↑p to p and ∞ to 0;

  • ENNReal.toReal := coe ∘ ENNReal.toNNReal sends ↑p, p : ℝ≥0 to (↑p : ℝ) and ∞ to 0;

  • ENNReal.ofReal := coe ∘ Real.toNNReal sends x : ℝ to ↑⟨max x 0, _⟩

  • ENNReal.neTopEquivNNReal is an equivalence between {a : ℝ≥0∞ // a ≠ 0} and ℝ≥0.

Implementation notes

We define a CanLift ℝ≥0∞ ℝ≥0 instance, so one of the ways to prove theorems about an ℝ≥0∞ number a is to consider the cases a = ∞ and a ≠ ∞, and use the tactic lift a to ℝ≥0 using ha in the second case. This instance is even more useful if one already has ha : a ≠ ∞ in the context, or if we have (f : α → ℝ≥0∞) (hf : ∀ x, f x ≠ ∞).

Notations

• ℝ≥0∞: the type of the extended nonnegative real numbers;
• ℝ≥0: the type of nonnegative real numbers [0, ∞); defined in Data.Real.NNReal;
• ∞: a localized notation in ENNReal for ⊤ : ℝ≥0∞.

def ENNReal : Type

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations

• ENNReal = WithTop NNReal

def ENNReal.«termℝ≥0∞» : Lean.ParserDescr

The extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.

Equations

• ENNReal.«termℝ≥0∞» = Lean.ParserDescr.node `ENNReal.termℝ≥0∞ 1024 (Lean.ParserDescr.symbol "ℝ≥0∞")

def ENNReal.«term∞» : Lean.ParserDescr

Notation for infinity as an ENNReal number.

Equations

• ENNReal.«term∞» = Lean.ParserDescr.node `ENNReal.term∞ 1024 (Lean.ParserDescr.symbol "∞")

instance ENNReal.instOrderBot : OrderBot ENNReal

Equations

• ENNReal.instOrderBot = inferInstanceAs (OrderBot (WithTop NNReal))

instance ENNReal.instBoundedOrder : BoundedOrder ENNReal

Equations

• ENNReal.instBoundedOrder = inferInstanceAs (BoundedOrder (WithTop NNReal))

instance ENNReal.instCharZero : CharZero ENNReal

Equations

• ENNReal.instCharZero = ⋯

noncomputable instance ENNReal.instCanonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ENNReal

Equations

• ENNReal.instCanonicallyOrderedCommSemiring = inferInstanceAs (CanonicallyOrderedCommSemiring (WithTop NNReal))

noncomputable instance ENNReal.instCompleteLinearOrder : CompleteLinearOrder ENNReal

Equations

• ENNReal.instCompleteLinearOrder = inferInstanceAs (CompleteLinearOrder (WithTop NNReal))

instance ENNReal.instDenselyOrdered : DenselyOrdered ENNReal

Equations

• ENNReal.instDenselyOrdered = ⋯

noncomputable instance ENNReal.instCanonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ENNReal

Equations

• ENNReal.instCanonicallyLinearOrderedAddCommMonoid = inferInstanceAs (CanonicallyLinearOrderedAddCommMonoid (WithTop NNReal))

noncomputable instance ENNReal.instSub : Sub ENNReal

Equations

• ENNReal.instSub = inferInstanceAs (Sub (WithTop NNReal))

noncomputable instance ENNReal.instOrderedSub : OrderedSub ENNReal

Equations

• ENNReal.instOrderedSub = ⋯

noncomputable instance ENNReal.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop ENNReal

Equations

• ENNReal.instLinearOrderedAddCommMonoidWithTop = inferInstanceAs (LinearOrderedAddCommMonoidWithTop (WithTop NNReal))

noncomputable instance ENNReal.instInv : Inv ENNReal

Equations

• ENNReal.instInv = { inv := fun (a : ENNReal) => sInf {b : ENNReal | 1 ≤ a * b} }

noncomputable instance ENNReal.instDivInvMonoid : DivInvMonoid ENNReal

Equations

• ENNReal.instDivInvMonoid = DivInvMonoid.mk ENNReal.instDivInvMonoid.proof_1 zpowRec ENNReal.instDivInvMonoid.proof_2 ENNReal.instDivInvMonoid.proof_3 ENNReal.instDivInvMonoid.proof_4

instance ENNReal.covariantClass_mul_le : CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x * x_1) fun (x x_1 : ENNReal) => x ≤ x_1

Equations

• ENNReal.covariantClass_mul_le = ⋯

instance ENNReal.covariantClass_add_le : CovariantClass ENNReal ENNReal (fun (x x_1 : ENNReal) => x + x_1) fun (x x_1 : ENNReal) => x ≤ x_1

Equations

• ENNReal.covariantClass_add_le = ⋯

noncomputable instance ENNReal.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ENNReal

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ENNReal.instUniqueAddUnits : Unique (AddUnits ENNReal)

Equations

• ENNReal.instUniqueAddUnits = { default := 0, uniq := ENNReal.instUniqueAddUnits.proof_1 }

instance ENNReal.instInhabited : Inhabited ENNReal

Equations

• ENNReal.instInhabited = { default := 0 }

@[match_pattern]

def ENNReal.ofNNReal : NNReal → ENNReal

Coercion from ℝ≥0 to ℝ≥0∞.

Equations

• ENNReal.ofNNReal = WithTop.some

instance ENNReal.instCoeNNReal : Coe NNReal ENNReal

Equations

• ENNReal.instCoeNNReal = { coe := ENNReal.ofNNReal }

def ENNReal.recTopCoe {C : ENNReal → Sort u_2} (top : C ⊤) (coe : (x : NNReal) → C ↑x) (x : ENNReal) : C x

A version of WithTop.recTopCoe that uses ENNReal.ofNNReal.

Equations

• ENNReal.recTopCoe top coe x = WithTop.recTopCoe top coe x

instance ENNReal.canLift : CanLift ENNReal NNReal ENNReal.ofNNReal fun (x : ENNReal) => x ≠ ⊤

Equations

• ENNReal.canLift = ⋯

@[simp]

theorem ENNReal.none_eq_top : none = ⊤

@[simp]

theorem ENNReal.some_eq_coe (a : NNReal) : some a = ↑a

@[simp]

theorem ENNReal.some_eq_coe' (a : NNReal) : ↑a = ↑a

theorem ENNReal.coe_injective : Function.Injective ENNReal.ofNNReal

@[simp]

theorem ENNReal.coe_inj {p : NNReal} {q : NNReal} : ↑p = ↑q ↔ p = q

theorem ENNReal.coe_ne_coe {p : NNReal} {q : NNReal} : ↑p ≠ ↑q ↔ p ≠ q

theorem ENNReal.range_coe' : Set.range ENNReal.ofNNReal = Set.Iio ⊤

theorem ENNReal.range_coe : Set.range ENNReal.ofNNReal = {⊤}ᶜ

def ENNReal.toNNReal : ENNReal → NNReal

toNNReal x returns x if it is real, otherwise 0.

Equations

• ENNReal.toNNReal = WithTop.untop' 0

def ENNReal.toReal (a : ENNReal) : ℝ

toReal x returns x if it is real, 0 otherwise.

Equations

• a.toReal = ↑a.toNNReal

noncomputable def ENNReal.ofReal (r : ℝ) : ENNReal

ofReal x returns x if it is nonnegative, 0 otherwise.

Equations

• ENNReal.ofReal r = ↑r.toNNReal

@[simp]

theorem ENNReal.toNNReal_coe {r : NNReal} : (↑r).toNNReal = r

@[simp]

theorem ENNReal.coe_toNNReal {a : ENNReal} : a ≠ ⊤ → ↑a.toNNReal = a

@[simp]

theorem ENNReal.ofReal_toReal {a : ENNReal} (h : a ≠ ⊤) : ENNReal.ofReal a.toReal = a

@[simp]

theorem ENNReal.toReal_ofReal {r : ℝ} (h : 0 ≤ r) : (ENNReal.ofReal r).toReal = r

theorem ENNReal.toReal_ofReal' {r : ℝ} : (ENNReal.ofReal r).toReal = max r 0

theorem ENNReal.coe_toNNReal_le_self {a : ENNReal} : ↑a.toNNReal ≤ a

theorem ENNReal.coe_nnreal_eq (r : NNReal) : ↑r = ENNReal.ofReal ↑r

theorem ENNReal.ofReal_eq_coe_nnreal {x : ℝ} (h : 0 ≤ x) : ENNReal.ofReal x = ↑⟨x, h⟩

@[simp]

theorem ENNReal.ofReal_coe_nnreal {p : NNReal} : ENNReal.ofReal ↑p = ↑p

@[simp]

theorem ENNReal.coe_zero : ↑0 = 0

@[simp]

theorem ENNReal.coe_one : ↑1 = 1

@[simp]

theorem ENNReal.toReal_nonneg {a : ENNReal} : 0 ≤ a.toReal

@[simp]

theorem ENNReal.top_toNNReal : ⊤.toNNReal = 0

@[simp]

theorem ENNReal.top_toReal : ⊤.toReal = 0

@[simp]

theorem ENNReal.one_toReal : ENNReal.toReal 1 = 1

@[simp]

theorem ENNReal.one_toNNReal : ENNReal.toNNReal 1 = 1

@[simp]

theorem ENNReal.coe_toReal (r : NNReal) : (↑r).toReal = ↑r

@[simp]

theorem ENNReal.zero_toNNReal : ENNReal.toNNReal 0 = 0

@[simp]

theorem ENNReal.zero_toReal : ENNReal.toReal 0 = 0

@[simp]

theorem ENNReal.ofReal_zero : ENNReal.ofReal 0 = 0

@[simp]

theorem ENNReal.ofReal_one : ENNReal.ofReal 1 = 1

theorem ENNReal.ofReal_toReal_le {a : ENNReal} : ENNReal.ofReal a.toReal ≤ a

theorem ENNReal.forall_ennreal {p : ENNReal → Prop} : (∀ (a : ENNReal), p a) ↔ (∀ (r : NNReal), p ↑r) ∧ p ⊤

theorem ENNReal.forall_ne_top {p : ENNReal → Prop} : (∀ (a : ENNReal), a ≠ ⊤ → p a) ↔ ∀ (r : NNReal), p ↑r

theorem ENNReal.exists_ne_top {p : ENNReal → Prop} : (∃ (a : ENNReal), a ≠ ⊤ ∧ p a) ↔ ∃ (r : NNReal), p ↑r

theorem ENNReal.toNNReal_eq_zero_iff (x : ENNReal) : x.toNNReal = 0 ↔ x = 0 ∨ x = ⊤

theorem ENNReal.toReal_eq_zero_iff (x : ENNReal) : x.toReal = 0 ↔ x = 0 ∨ x = ⊤

theorem ENNReal.toNNReal_ne_zero {a : ENNReal} : a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤

theorem ENNReal.toReal_ne_zero {a : ENNReal} : a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ⊤

theorem ENNReal.toNNReal_eq_one_iff (x : ENNReal) : x.toNNReal = 1 ↔ x = 1

theorem ENNReal.toReal_eq_one_iff (x : ENNReal) : x.toReal = 1 ↔ x = 1

theorem ENNReal.toNNReal_ne_one {a : ENNReal} : a.toNNReal ≠ 1 ↔ a ≠ 1

theorem ENNReal.toReal_ne_one {a : ENNReal} : a.toReal ≠ 1 ↔ a ≠ 1

@[simp]

theorem ENNReal.coe_ne_top {r : NNReal} : ↑r ≠ ⊤

@[simp]

theorem ENNReal.top_ne_coe {r : NNReal} : ⊤ ≠ ↑r

@[simp]

theorem ENNReal.coe_lt_top {r : NNReal} : ↑r < ⊤

@[simp]

theorem ENNReal.ofReal_ne_top {r : ℝ} : ENNReal.ofReal r ≠ ⊤

@[simp]

theorem ENNReal.ofReal_lt_top {r : ℝ} : ENNReal.ofReal r < ⊤

@[simp]

theorem ENNReal.top_ne_ofReal {r : ℝ} : ⊤ ≠ ENNReal.ofReal r

@[simp]

theorem ENNReal.ofReal_toReal_eq_iff {a : ENNReal} : ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤

@[simp]

theorem ENNReal.toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ a

@[simp]

theorem ENNReal.zero_ne_top : 0 ≠ ⊤

@[simp]

theorem ENNReal.top_ne_zero : ⊤ ≠ 0

@[simp]

theorem ENNReal.one_ne_top : 1 ≠ ⊤

@[simp]

theorem ENNReal.top_ne_one : ⊤ ≠ 1

@[simp]

theorem ENNReal.zero_lt_top : 0 < ⊤

@[simp]

theorem ENNReal.coe_le_coe {r : NNReal} {q : NNReal} : ↑r ≤ ↑q ↔ r ≤ q

@[simp]

theorem ENNReal.coe_lt_coe {r : NNReal} {q : NNReal} : ↑r < ↑q ↔ r < q

theorem ENNReal.coe_le_coe_of_le {r : NNReal} {q : NNReal} : r ≤ q → ↑r ≤ ↑q

Alias of the reverse direction of ENNReal.coe_le_coe.

theorem ENNReal.coe_lt_coe_of_lt {r : NNReal} {q : NNReal} : r < q → ↑r < ↑q

Alias of the reverse direction of ENNReal.coe_lt_coe.

theorem ENNReal.coe_mono : Monotone ENNReal.ofNNReal

theorem ENNReal.coe_strictMono : StrictMono ENNReal.ofNNReal

@[simp]

theorem ENNReal.coe_eq_zero {r : NNReal} : ↑r = 0 ↔ r = 0

@[simp]

theorem ENNReal.zero_eq_coe {r : NNReal} : 0 = ↑r ↔ 0 = r

@[simp]

theorem ENNReal.coe_eq_one {r : NNReal} : ↑r = 1 ↔ r = 1

@[simp]

theorem ENNReal.one_eq_coe {r : NNReal} : 1 = ↑r ↔ 1 = r

@[simp]

theorem ENNReal.coe_pos {r : NNReal} : 0 < ↑r ↔ 0 < r

theorem ENNReal.coe_ne_zero {r : NNReal} : ↑r ≠ 0 ↔ r ≠ 0

theorem ENNReal.coe_ne_one {r : NNReal} : ↑r ≠ 1 ↔ r ≠ 1

@[simp]

theorem ENNReal.coe_add (x : NNReal) (y : NNReal) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem ENNReal.coe_mul (x : NNReal) (y : NNReal) : ↑(x * y) = ↑x * ↑y

theorem ENNReal.coe_nsmul (n : ℕ) (x : NNReal) : ↑(n • x) = n • ↑x

@[simp]

theorem ENNReal.coe_pow (x : NNReal) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem ENNReal.coe_ofNat (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

theorem ENNReal.coe_two : ↑2 = 2

theorem ENNReal.toNNReal_eq_toNNReal_iff (x : ENNReal) (y : ENNReal) : x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

theorem ENNReal.toReal_eq_toReal_iff (x : ENNReal) (y : ENNReal) : x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

theorem ENNReal.toNNReal_eq_toNNReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toNNReal = y.toNNReal ↔ x = y

theorem ENNReal.toReal_eq_toReal_iff' {x : ENNReal} {y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toReal = y.toReal ↔ x = y

theorem ENNReal.one_lt_two : 1 < 2

@[simp]

theorem ENNReal.two_ne_top : 2 ≠ ⊤

@[simp]

theorem ENNReal.two_lt_top : 2 < ⊤

instance fact_one_le_one_ennreal : Fact (1 ≤ 1)

(1 : ℝ≥0∞) ≤ 1, recorded as a Fact for use with Lp spaces.

Equations

• fact_one_le_one_ennreal = ⋯

instance fact_one_le_two_ennreal : Fact (1 ≤ 2)

(1 : ℝ≥0∞) ≤ 2, recorded as a Fact for use with Lp spaces.

Equations

• fact_one_le_two_ennreal = ⋯

instance fact_one_le_top_ennreal : Fact (1 ≤ ⊤)

(1 : ℝ≥0∞) ≤ ∞, recorded as a Fact for use with Lp spaces.

Equations

• fact_one_le_top_ennreal = ⋯

def ENNReal.neTopEquivNNReal : ↑{a : ENNReal | a ≠ ⊤} ≃ NNReal

The set of numbers in ℝ≥0∞ that are not equal to ∞ is equivalent to ℝ≥0.

Equations

• ENNReal.neTopEquivNNReal = { toFun := fun (x : ↑{a : ENNReal | a ≠ ⊤}) => (↑x).toNNReal, invFun := fun (x : NNReal) => ⟨↑x, ⋯⟩, left_inv := ENNReal.neTopEquivNNReal.proof_1, right_inv := ⋯ }

theorem ENNReal.cinfi_ne_top {α : Type u_1} [InfSet α] (f : ENNReal → α) : ⨅ (x : { x : ENNReal // x ≠ ⊤ }), f ↑x = ⨅ (x : NNReal), f ↑x

theorem ENNReal.iInf_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNReal → α) : ⨅ (x : ENNReal), ⨅ (_ : x ≠ ⊤), f x = ⨅ (x : NNReal), f ↑x

theorem ENNReal.csupr_ne_top {α : Type u_1} [SupSet α] (f : ENNReal → α) : ⨆ (x : { x : ENNReal // x ≠ ⊤ }), f ↑x = ⨆ (x : NNReal), f ↑x

theorem ENNReal.iSup_ne_top {α : Type u_1} [CompleteLattice α] (f : ENNReal → α) : ⨆ (x : ENNReal), ⨆ (_ : x ≠ ⊤), f x = ⨆ (x : NNReal), f ↑x

theorem ENNReal.iInf_ennreal {α : Type u_2} [CompleteLattice α] {f : ENNReal → α} : ⨅ (n : ENNReal), f n = (⨅ (n : NNReal), f ↑n) ⊓ f ⊤

theorem ENNReal.iSup_ennreal {α : Type u_2} [CompleteLattice α] {f : ENNReal → α} : ⨆ (n : ENNReal), f n = (⨆ (n : NNReal), f ↑n) ⊔ f ⊤

def ENNReal.ofNNRealHom : NNReal →+* ENNReal

Coercion ℝ≥0 → ℝ≥0∞ as a RingHom.

Equations

• ENNReal.ofNNRealHom = { toFun := some, map_one' := ENNReal.coe_one, map_mul' := ⋯, map_zero' := ENNReal.coe_zero, map_add' := ⋯ }

@[simp]

theorem ENNReal.coe_ofNNRealHom : ⇑ENNReal.ofNNRealHom = some

@[simp]

theorem ENNReal.coe_indicator {α : Type u_2} (s : Set α) (f : α → NNReal) (a : α) : ↑(s.indicator f a) = s.indicator (fun (x : α) => ↑(f x)) a

theorem ENNReal.bot_eq_zero : ⊥ = 0

theorem ENNReal.not_top_le_coe {r : NNReal} : ¬⊤ ≤ ↑r

@[simp]

theorem ENNReal.one_le_coe_iff {r : NNReal} : 1 ≤ ↑r ↔ 1 ≤ r

@[simp]

theorem ENNReal.coe_le_one_iff {r : NNReal} : ↑r ≤ 1 ↔ r ≤ 1

@[simp]

theorem ENNReal.coe_lt_one_iff {p : NNReal} : ↑p < 1 ↔ p < 1

@[simp]

theorem ENNReal.one_lt_coe_iff {p : NNReal} : 1 < ↑p ↔ 1 < p

@[simp]

theorem ENNReal.coe_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem ENNReal.ofReal_natCast (n : ℕ) : ENNReal.ofReal ↑n = ↑n

@[simp]

theorem ENNReal.ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.ofReal (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem ENNReal.natCast_ne_top (n : ℕ) : ↑n ≠ ⊤

@[simp]

theorem ENNReal.top_ne_natCast (n : ℕ) : ⊤ ≠ ↑n

@[simp]

theorem ENNReal.one_lt_top : 1 < ⊤

@[simp]

theorem ENNReal.toNNReal_nat (n : ℕ) : (↑n).toNNReal = ↑n

@[simp]

theorem ENNReal.toReal_nat (n : ℕ) : (↑n).toReal = ↑n

@[simp]

theorem ENNReal.toReal_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toReal = OfNat.ofNat n

theorem ENNReal.le_coe_iff {a : ENNReal} {r : NNReal} : a ≤ ↑r ↔ ∃ (p : NNReal), a = ↑p ∧ p ≤ r

theorem ENNReal.coe_le_iff {a : ENNReal} {r : NNReal} : ↑r ≤ a ↔ ∀ (p : NNReal), a = ↑p → r ≤ p

theorem ENNReal.lt_iff_exists_coe {a : ENNReal} {b : ENNReal} : a < b ↔ ∃ (p : NNReal), a = ↑p ∧ ↑p < b

theorem ENNReal.toReal_le_coe_of_le_coe {a : ENNReal} {b : NNReal} (h : a ≤ ↑b) : a.toReal ≤ ↑b

@[simp]

theorem ENNReal.coe_finset_sup {α : Type u_1} {s : Finset α} {f : α → NNReal} : ↑(s.sup f) = s.sup fun (x : α) => ↑(f x)

@[simp]

theorem ENNReal.max_eq_zero_iff {a : ENNReal} {b : ENNReal} : max a b = 0 ↔ a = 0 ∧ b = 0

theorem ENNReal.max_zero_left {a : ENNReal} : max 0 a = a

theorem ENNReal.max_zero_right {a : ENNReal} : max a 0 = a

@[simp]

theorem ENNReal.sup_eq_max {a : ENNReal} {b : ENNReal} : a ⊔ b = max a b

theorem ENNReal.lt_iff_exists_rat_btwn {a : ENNReal} {b : ENNReal} : a < b ↔ ∃ (q : ℚ), 0 ≤ q ∧ a < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

theorem ENNReal.lt_iff_exists_real_btwn {a : ENNReal} {b : ENNReal} : a < b ↔ ∃ (r : ℝ), 0 ≤ r ∧ a < ENNReal.ofReal r ∧ ENNReal.ofReal r < b

theorem ENNReal.lt_iff_exists_nnreal_btwn {a : ENNReal} {b : ENNReal} : a < b ↔ ∃ (r : NNReal), a < ↑r ∧ ↑r < b

theorem ENNReal.lt_iff_exists_add_pos_lt {a : ENNReal} {b : ENNReal} : a < b ↔ ∃ (r : NNReal), 0 < r ∧ a + ↑r < b

theorem ENNReal.le_of_forall_pos_le_add {a : ENNReal} {b : ENNReal} (h : ∀ (ε : NNReal), 0 < ε → b < ⊤ → a ≤ b + ↑ε) : a ≤ b

theorem ENNReal.natCast_lt_coe {r : NNReal} {n : ℕ} : ↑n < ↑r ↔ ↑n < r

theorem ENNReal.coe_lt_natCast {r : NNReal} {n : ℕ} : ↑r < ↑n ↔ r < ↑n

@[deprecated ENNReal.coe_natCast]

theorem ENNReal.coe_nat (n : ℕ) : ↑↑n = ↑n

Alias of ENNReal.coe_natCast.

@[deprecated ENNReal.ofReal_natCast]

theorem ENNReal.ofReal_coe_nat (n : ℕ) : ENNReal.ofReal ↑n = ↑n

Alias of ENNReal.ofReal_natCast.

@[deprecated ENNReal.natCast_ne_top]

theorem ENNReal.nat_ne_top (n : ℕ) : ↑n ≠ ⊤

Alias of ENNReal.natCast_ne_top.

@[deprecated ENNReal.top_ne_natCast]

theorem ENNReal.top_ne_nat (n : ℕ) : ⊤ ≠ ↑n

Alias of ENNReal.top_ne_natCast.

@[deprecated ENNReal.natCast_lt_coe]

theorem ENNReal.coe_nat_lt_coe {r : NNReal} {n : ℕ} : ↑n < ↑r ↔ ↑n < r

Alias of ENNReal.natCast_lt_coe.

@[deprecated ENNReal.coe_lt_natCast]

theorem ENNReal.coe_lt_coe_nat {r : NNReal} {n : ℕ} : ↑r < ↑n ↔ r < ↑n

Alias of ENNReal.coe_lt_natCast.

theorem ENNReal.exists_nat_gt {r : ENNReal} (h : r ≠ ⊤) : ∃ (n : ℕ), r < ↑n

@[simp]

theorem ENNReal.iUnion_Iio_coe_nat : ⋃ (n : ℕ), Set.Iio ↑n = {⊤}ᶜ

@[simp]

theorem ENNReal.iUnion_Iic_coe_nat : ⋃ (n : ℕ), Set.Iic ↑n = {⊤}ᶜ

@[simp]

theorem ENNReal.iUnion_Ioc_coe_nat {a : ENNReal} : ⋃ (n : ℕ), Set.Ioc a ↑n = Set.Ioi a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Ioo_coe_nat {a : ENNReal} : ⋃ (n : ℕ), Set.Ioo a ↑n = Set.Ioi a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Icc_coe_nat {a : ENNReal} : ⋃ (n : ℕ), Set.Icc a ↑n = Set.Ici a \ {⊤}

@[simp]

theorem ENNReal.iUnion_Ico_coe_nat {a : ENNReal} : ⋃ (n : ℕ), Set.Ico a ↑n = Set.Ici a \ {⊤}

@[simp]

theorem ENNReal.iInter_Ici_coe_nat : ⋂ (n : ℕ), Set.Ici ↑n = {⊤}

@[simp]

theorem ENNReal.iInter_Ioi_coe_nat : ⋂ (n : ℕ), Set.Ioi ↑n = {⊤}

@[simp]

theorem ENNReal.coe_min (r : NNReal) (p : NNReal) : ↑(min r p) = min ↑r ↑p

@[simp]

theorem ENNReal.coe_max (r : NNReal) (p : NNReal) : ↑(max r p) = max ↑r ↑p

theorem ENNReal.le_of_top_imp_top_of_toNNReal_le {a : ENNReal} {b : ENNReal} (h : a = ⊤ → b = ⊤) (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b

@[simp]

theorem ENNReal.abs_toReal {x : ENNReal} : |x.toReal| = x.toReal

theorem ENNReal.coe_sSup {s : Set NNReal} : BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a

theorem ENNReal.coe_sInf {s : Set NNReal} (hs : s.Nonempty) : ↑(sInf s) = ⨅ a ∈ s, ↑a

theorem ENNReal.coe_iSup {ι : Sort u_3} {f : ι → NNReal} (hf : BddAbove (Set.range f)) : ↑(iSup f) = ⨆ (a : ι), ↑(f a)

theorem ENNReal.coe_iInf {ι : Sort u_3} [Nonempty ι] (f : ι → NNReal) : ↑(iInf f) = ⨅ (a : ι), ↑(f a)

theorem ENNReal.coe_mem_upperBounds {r : NNReal} {s : Set NNReal} : ↑r ∈ upperBounds (ENNReal.ofNNReal '' s) ↔ r ∈ upperBounds s

theorem ENNReal.iSup_coe_eq_top {ι : Sort u_2} {f : ι → NNReal} : ⨆ (i : ι), ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)

theorem ENNReal.iSup_coe_lt_top {ι : Sort u_2} {f : ι → NNReal} : ⨆ (i : ι), ↑(f i) < ⊤ ↔ BddAbove (Set.range f)

theorem ENNReal.iInf_coe_eq_top {ι : Sort u_2} {f : ι → NNReal} : ⨅ (i : ι), ↑(f i) = ⊤ ↔ IsEmpty ι

theorem ENNReal.iInf_coe_lt_top {ι : Sort u_2} {f : ι → NNReal} : ⨅ (i : ι), ↑(f i) < ⊤ ↔ Nonempty ι

theorem Set.OrdConnected.preimage_coe_nnreal_ennreal {u : Set ENNReal} (h : u.OrdConnected) : (ENNReal.ofNNReal ⁻¹' u).OrdConnected

theorem Set.OrdConnected.image_coe_nnreal_ennreal {t : Set NNReal} (h : t.OrdConnected) : (ENNReal.ofNNReal '' t).OrdConnected

theorem Set.OrdConnected.preimage_ennreal_ofReal {u : Set ENNReal} (h : u.OrdConnected) : (ENNReal.ofReal ⁻¹' u).OrdConnected

theorem Set.OrdConnected.image_ennreal_ofReal {s : Set ℝ} (h : s.OrdConnected) : (ENNReal.ofReal '' s).OrdConnected

def Mathlib.Meta.Positivity.evalENNRealtoReal : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.toReal.

def Mathlib.Meta.Positivity.evalENNRealOfNNReal : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: ENNReal.ofNNReal.

@[deprecated le_inv_smul_iff_of_pos]

theorem ENNReal.le_inv_smul_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) : b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Alias of le_inv_smul_iff_of_pos.

@[deprecated inv_smul_le_iff_of_pos]

theorem ENNReal.inv_smul_le_iff_of_pos {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} {b₂ : β} [GroupWithZero α] [Preorder α] [Preorder β] [MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) : a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Alias of inv_smul_le_iff_of_pos.