Mathlib.Data.ENNReal.Basic

ENNReal definition

Full source

/-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
  and is relevant as the codomain of a measure. -/
def ENNReal := WithTop ℝ≥0
  deriving Zero, Top, AddCommMonoidWithOne, SemilatticeSup, DistribLattice, Nontrivial

Extended nonnegative real numbers

Informal description

The type $\mathbb{R}_{\geq 0} \cup \{\infty\}$ of extended nonnegative real numbers, defined as $\mathbb{R}_{\geq 0}$ with a top element $\infty$ adjoined. This represents the interval $[0, +\infty]$ and serves as the codomain for measures in measure theory and extended distances in extended metric spaces.

ENNReal.termℝ≥0∞ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped[ENNReal] notation "ℝ≥0∞" => ENNReal

Notation for extended nonnegative real numbers

Informal description

The notation `ℝ≥0∞` represents the type of extended nonnegative real numbers, which is defined as `WithTop ℝ≥0` (the nonnegative real numbers extended with a top element ∞). This type represents the interval `[0, +∞]` and is used as the codomain for measures in measure theory and extended distances in extended metric spaces.

ENNReal.term∞ definition

: Lean.ParserDescr✝

Full source

/-- Notation for infinity as an `ENNReal` number. -/
scoped[ENNReal] notation "∞" => (⊤ : ENNReal)

Infinity notation in extended nonnegative reals

Informal description

The notation `∞` represents the infinity element in the extended nonnegative real numbers `ℝ≥0∞`, which is defined as the top element `⊤` of this type.

ENNReal.instOrderBot instance

: OrderBot ℝ≥0∞

Full source

instance : OrderBot ℝ≥0∞ := inferInstanceAs (OrderBot (WithTop ℝ≥0))

Bottom Element in Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an order with a bottom element, where the bottom element is $0$.

ENNReal.instOrderTop instance

: OrderTop ℝ≥0∞

Full source

instance : OrderTop ℝ≥0∞ := inferInstanceAs (OrderTop (WithTop ℝ≥0))

Extended Nonnegative Reals as an Ordered Top

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an ordered set with a greatest element $\infty$.

ENNReal.instBoundedOrder instance

: BoundedOrder ℝ≥0∞

Full source

instance : BoundedOrder ℝ≥0∞ := inferInstanceAs (BoundedOrder (WithTop ℝ≥0))

Bounded Order Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a bounded order, with $\infty$ as the greatest element and $0$ as the least element.

ENNReal.instCharZero instance

: CharZero ℝ≥0∞

Full source

instance : CharZero ℝ≥0∞ := inferInstanceAs (CharZero (WithTop ℝ≥0))

Characteristic Zero Property of Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a monoid with one of characteristic zero. That is, the canonical map from the natural numbers $\mathbb{N}$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is injective.

ENNReal.instMin instance

: Min ℝ≥0∞

Full source

instance : Min ℝ≥0∞ := SemilatticeInf.toMin

Minimum Operation on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a canonical minimum operation, where for any two elements $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the minimum $\min(a, b)$ is defined as the infimum of $a$ and $b$ with respect to the natural order on $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.instMax instance

: Max ℝ≥0∞

Full source

instance : Max ℝ≥0∞ := SemilatticeSup.toMax

Maximum Operation on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a canonical maximum operation, where for any two elements $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the maximum $\max(a, b)$ is defined as the supremum of $a$ and $b$ with respect to the natural order on $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.instCommSemiring instance

: CommSemiring ℝ≥0∞

Full source

noncomputable instance : CommSemiring ℝ≥0∞ :=
  inferInstanceAs (CommSemiring (WithTop ℝ≥0))

Commutative Semiring Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a commutative semiring, where addition and multiplication are defined in the natural way for finite values and extended appropriately for infinity.

ENNReal.instPartialOrder instance

: PartialOrder ℝ≥0∞

Full source

instance : PartialOrder ℝ≥0∞ :=
  inferInstanceAs (PartialOrder (WithTop ℝ≥0))

Partial Order on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a partial order where the order is defined by extending the natural order on $\mathbb{R}_{\geq 0}$ with $\infty$ as the greatest element. Specifically, for any $a, b \in \mathbb{R}_{\geq 0}$, we have $a \leq b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $a \leq b$ in $\mathbb{R}_{\geq 0}$, and $\infty$ is greater than or equal to all elements.

ENNReal.instIsOrderedRing instance

: IsOrderedRing ℝ≥0∞

Full source

instance : IsOrderedRing ℝ≥0∞ :=
  inferInstanceAs (IsOrderedRing (WithTop ℝ≥0))

Ordered Ring Structure on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an ordered ring, where the order and ring operations are compatible in the sense that addition and multiplication preserve the order relation.

ENNReal.instCanonicallyOrderedAdd instance

: CanonicallyOrderedAdd ℝ≥0∞

Full source

instance : CanonicallyOrderedAdd ℝ≥0∞ :=
  inferInstanceAs (CanonicallyOrderedAdd (WithTop ℝ≥0))

Canonical Ordering on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a canonically ordered additive monoid. This means that for any two elements $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a \leq b$ holds if and only if there exists an element $c$ such that $b = a + c$.

ENNReal.instNoZeroDivisors instance

: NoZeroDivisors ℝ≥0∞

Full source

instance : NoZeroDivisors ℝ≥0∞ :=
  inferInstanceAs (NoZeroDivisors (WithTop ℝ≥0))

No Zero Divisors in Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have no zero divisors. That is, for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \cdot b = 0$, then either $a = 0$ or $b = 0$.

ENNReal.instCompleteLinearOrder instance

: CompleteLinearOrder ℝ≥0∞

Full source

noncomputable instance : CompleteLinearOrder ℝ≥0∞ :=
  inferInstanceAs (CompleteLinearOrder (WithTop ℝ≥0))

Complete Linear Order Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a complete linear order, where the order is defined by extending the natural order on $\mathbb{R}_{\geq 0}$ with $\infty$ as the greatest element. This means every subset has both a supremum and an infimum, and the order is total.

ENNReal.instDenselyOrdered instance

: DenselyOrdered ℝ≥0∞

Full source

instance : DenselyOrdered ℝ≥0∞ := inferInstanceAs (DenselyOrdered (WithTop ℝ≥0))

Dense Order on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a densely ordered set. That is, for any two elements $a < b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists an element $x$ such that $a < x < b$.

ENNReal.instAddCommMonoid instance

: AddCommMonoid ℝ≥0∞

Full source

instance : AddCommMonoid ℝ≥0∞ :=
  inferInstanceAs (AddCommMonoid (WithTop ℝ≥0))

Additive Commutative Monoid Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an additive commutative monoid, where addition is defined in the natural way for finite values and extended to infinity by $a + \infty = \infty + a = \infty$ for any $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.instLinearOrder instance

: LinearOrder ℝ≥0∞

Full source

noncomputable instance : LinearOrder ℝ≥0∞ :=
  inferInstanceAs (LinearOrder (WithTop ℝ≥0))

Linear Order on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a linear order, where the order is extended from the natural order on $\mathbb{R}_{\geq 0}$ by declaring $\infty$ to be the greatest element.

ENNReal.instIsOrderedAddMonoid instance

: IsOrderedAddMonoid ℝ≥0∞

Full source

instance : IsOrderedAddMonoid ℝ≥0∞ :=
  inferInstanceAs (IsOrderedAddMonoid (WithTop ℝ≥0))

Ordered Additive Monoid Structure on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an ordered additive monoid, where the addition operation is monotone with respect to the partial order. Specifically, for any $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b$ then $a + c \leq b + c$ and $c + a \leq c + b$.

ENNReal.instSub instance

: Sub ℝ≥0∞

Full source

instance instSub : Sub ℝ≥0∞ := inferInstanceAs (Sub (WithTop ℝ≥0))

Subtraction on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ are equipped with a subtraction operation defined as the minimal $d$ such that $a \leq d + b$. This operation satisfies: - For $p, q \in \mathbb{R}_{\geq 0}$, $\uparrow p - \uparrow q = \uparrow (p - q)$ - $\infty - \uparrow p = \infty$ - $\uparrow p - \infty = \infty - \infty = 0$

ENNReal.instOrderedSub instance

: OrderedSub ℝ≥0∞

Full source

instance : OrderedSub ℝ≥0∞ := inferInstanceAs (OrderedSub (WithTop ℝ≥0))

Ordered Subtraction on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form an ordered structure with subtraction, where the subtraction operation is compatible with the order. Specifically, for any $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \leq b$, then $a - c \leq b - c$ whenever the subtraction is defined.

ENNReal.instLinearOrderedAddCommMonoidWithTop instance

: LinearOrderedAddCommMonoidWithTop ℝ≥0∞

Full source

noncomputable instance : LinearOrderedAddCommMonoidWithTop ℝ≥0∞ :=
  inferInstanceAs (LinearOrderedAddCommMonoidWithTop (WithTop ℝ≥0))

Linearly Ordered Commutative Additive Monoid Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a linearly ordered commutative additive monoid with a top element $\infty$, where the addition operation extends the usual addition on $\mathbb{R}_{\geq 0}$ and satisfies $a + \infty = \infty + a = \infty$ for all $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.instInv instance

: Inv ℝ≥0∞

Full source

noncomputable instance : Inv ℝ≥0∞ := ⟨fun a => sInf { b | 1 ≤ a * b }⟩

Inversion Operation on Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have an inversion operation defined by: - For $x \in \mathbb{R}_{>0}$, $x^{-1} = \frac{1}{x}$; - $0^{-1} = \infty$; - $\infty^{-1} = 0$. This operation makes $\mathbb{R}_{\geq 0} \cup \{\infty\}$ into a structure with inverses.

ENNReal.instDivInvMonoid instance

: DivInvMonoid ℝ≥0∞

Full source

noncomputable instance : DivInvMonoid ℝ≥0∞ where

Division and Inversion Monoid Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a division and inversion monoid, where division and inversion are defined as follows: - For $x, y \in \mathbb{R}_{>0}$, $x / y = x \cdot y^{-1}$ with $y^{-1} = \frac{1}{y}$; - $0^{-1} = \infty$ and $\infty^{-1} = 0$; - $0 / y = 0$ for $y \neq 0$, $x / 0 = \infty$ for $x \neq 0$, and $0 / 0$ is undefined (treated as $0$ by convention); - $x / \infty = 0$ for $x \neq \infty$, $\infty / y = \infty$ for $y \neq \infty$, and $\infty / \infty$ is undefined (treated as $0$ by convention). This structure extends the usual division and inversion operations on $\mathbb{R}_{>0}$ to include $\infty$ and $0$ in a way that is consistent with limits and measure theory.

ENNReal.instLinearOrderedCommMonoidWithZero instance

: LinearOrderedCommMonoidWithZero ℝ≥0∞

Full source

noncomputable instance : LinearOrderedCommMonoidWithZero ℝ≥0∞ :=
  { inferInstanceAs (LinearOrderedAddCommMonoidWithTop ℝ≥0∞),
      inferInstanceAs (CommSemiring ℝ≥0∞) with
    bot_le _ := bot_le
    mul_le_mul_left := fun _ _ => mul_le_mul_left'
    zero_le_one := zero_le 1 }

Linearly Ordered Commutative Monoid with Zero Structure on Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a linearly ordered commutative monoid with zero, where the multiplication operation extends the usual multiplication on $\mathbb{R}_{\geq 0}$ and satisfies $0 \cdot \infty = \infty \cdot 0 = 0$, and $a \cdot \infty = \infty \cdot a = \infty$ for $a \neq 0$. The order is the natural extension of the order on $\mathbb{R}_{\geq 0}$ with $\infty$ as the greatest element.

ENNReal.instUniqueAddUnits instance

: Unique (AddUnits ℝ≥0∞)

Full source

instance : Unique (AddUnits ℝ≥0∞) where
  default := 0
  uniq a := AddUnits.ext <| le_zero_iff.1 <| by rw [← a.add_neg]; exact le_self_add

Uniqueness of Additive Units in Extended Nonnegative Reals

Informal description

The additive units of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ form a unique structure. That is, there is exactly one additive unit in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, which is the element $0$.

ENNReal.instInhabited instance

: Inhabited ℝ≥0∞

Full source

instance : Inhabited ℝ≥0∞ := ⟨0⟩

Inhabited Type of Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is an inhabited type, meaning it has a default element.

ENNReal.ofNNReal definition

: ℝ≥0 → ℝ≥0∞

Full source

/-- Coercion from `ℝ≥0` to `ℝ≥0∞`. -/
@[coe, match_pattern] def ofNNReal : ℝ≥0 → ℝ≥0∞ := WithTop.some

Inclusion of nonnegative reals into extended nonnegative reals

Informal description

The canonical injection from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, mapping each $x \in \mathbb{R}_{\geq 0}$ to itself in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.instCoeNNReal instance

: Coe ℝ≥0 ℝ≥0∞

Full source

instance : Coe ℝ≥0 ℝ≥0∞ := ⟨ofNNReal⟩

Canonical Coercion from Nonnegative Reals to Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a canonical coercion from the nonnegative real numbers $\mathbb{R}_{\geq 0}$, where each $x \in \mathbb{R}_{\geq 0}$ is mapped to itself in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.recTopCoe definition

{C : ℝ≥0∞ → Sort*} (top : C ∞) (coe : ∀ x : ℝ≥0, C x) (x : ℝ≥0∞) : C x

Full source

/-- A version of `WithTop.recTopCoe` that uses `ENNReal.ofNNReal`. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
def recTopCoe {C : ℝ≥0∞ → Sort*} (top : C ∞) (coe : ∀ x : ℝ≥0, C x) (x : ℝ≥0∞) : C x :=
  WithTop.recTopCoe top coe x

Recursor for extended nonnegative real numbers by cases on $\infty$ and nonnegative reals

Informal description

The recursor for extended nonnegative real numbers, which allows defining a function by cases on the element $\infty$ and the canonical injection of nonnegative real numbers. Specifically, given a term `top` of type `C ∞` and a function `coe : ∀ x : ℝ≥0, C x`, it defines a function `f : ℝ≥0∞ → C` such that `f ∞ = top` and `f (x) = coe x` for any $x \in \mathbb{R}_{\geq 0}$.

ENNReal.canLift instance

: CanLift ℝ≥0∞ ℝ≥0 ofNNReal (· ≠ ∞)

Full source

instance canLift : CanLift ℝ≥0∞ ℝ≥0 ofNNReal (· ≠ ∞) := WithTop.canLift

Lifting Condition for Extended Nonnegative Real Numbers

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$, then $a$ can be lifted to a nonnegative real number via the canonical inclusion map $\mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.none_eq_top theorem

: (none : ℝ≥0∞) = ∞

Full source

@[simp] theorem none_eq_top : (none : ℝ≥0∞) = ∞ := rfl

None Value Represents Infinity in Extended Nonnegative Reals

Informal description

The `none` value in the type of extended nonnegative real numbers is equal to the infinity element $\infty$.

ENNReal.some_eq_coe theorem

(a : ℝ≥0) : (Option.some a : ℝ≥0∞) = (↑a : ℝ≥0∞)

Full source

@[simp] theorem some_eq_coe (a : ℝ≥0) : (Option.some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl

Equality of Option Injection and Coercion for Nonnegative Reals in Extended Nonnegative Reals

Informal description

For any nonnegative real number $a \in \mathbb{R}_{\geq 0}$, the injection of $a$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via `Option.some` is equal to the canonical coercion of $a$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\text{some}(a) = a$.

ENNReal.some_eq_coe' theorem

(a : ℝ≥0) : (WithTop.some a : ℝ≥0∞) = (↑a : ℝ≥0∞)

Full source

@[simp] theorem some_eq_coe' (a : ℝ≥0) : (WithTop.some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl

Equality of Injection and Coercion for Nonnegative Reals in Extended Nonnegative Reals

Informal description

For any nonnegative real number $a \in \mathbb{R}_{\geq 0}$, the injection of $a$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via `WithTop.some` is equal to the canonical coercion of $a$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\text{some}(a) = a$.

ENNReal.coe_injective theorem

: Injective ((↑) : ℝ≥0 → ℝ≥0∞)

Full source

lemma coe_injective : Injective ((↑) : ℝ≥0 → ℝ≥0∞) := WithTop.coe_injective

Injectivity of the Canonical Injection from Nonnegative Reals to Extended Nonnegative Reals

Informal description

The canonical injection function $(↑) : \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is injective. That is, for any $p, q \in \mathbb{R}_{\geq 0}$, if $p = q$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, then $p = q$ in $\mathbb{R}_{\geq 0}$.

ENNReal.coe_inj theorem

: (p : ℝ≥0∞) = q ↔ p = q

Full source

@[simp, norm_cast] lemma coe_inj : (p : ℝ≥0∞) = q ↔ p = q := coe_injective.eq_iff

Injection Equality Criterion for Extended Nonnegative Reals: $\uparrow p = \uparrow q \leftrightarrow p = q$

Informal description

For any two extended nonnegative real numbers $p$ and $q$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the canonical injection of $p$ equals the canonical injection of $q$ if and only if $p = q$.

ENNReal.coe_ne_coe theorem

: (p : ℝ≥0∞) ≠ q ↔ p ≠ q

Full source

lemma coe_ne_coe : (p : ℝ≥0∞) ≠ q(p : ℝ≥0∞) ≠ q ↔ p ≠ q := coe_inj.not

Inequality of Canonical Injections in Extended Nonnegative Reals: $\uparrow p \neq \uparrow q \leftrightarrow p \neq q$

Informal description

For any two nonnegative real numbers $p$ and $q$, the canonical injections $\uparrow p$ and $\uparrow q$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ are unequal if and only if $p \neq q$.

ENNReal.range_coe' theorem

: range ofNNReal = Iio ∞

Full source

theorem range_coe' : range ofNNReal = Iio ∞ := WithTop.range_coe

Range of Inclusion Map in Extended Nonnegative Reals Equals $[0, \infty)$

Informal description

The range of the canonical inclusion map $\text{ofNNReal} : \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the interval $[0, \infty)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, i.e., $\text{range}(\text{ofNNReal}) = [0, \infty)$.

ENNReal.range_coe theorem

: range ofNNReal = {∞}ᶜ

Full source

theorem range_coe : range ofNNReal = {∞}{∞}ᶜ := (isCompl_range_some_none ℝ≥0).symm.compl_eq.symm

Range of Nonnegative Real Injection is Complement of Infinity in Extended Nonnegative Reals

Informal description

The range of the canonical injection from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the complement of the singleton set $\{\infty\}$. In other words, $\text{range}(\text{ofNNReal}) = \mathbb{R}_{\geq 0} \cup \{\infty\} \setminus \{\infty\}$.

ENNReal.instNNRatCast instance

: NNRatCast ℝ≥0∞

Full source

instance : NNRatCast ℝ≥0∞ where
  nnratCast r := ofNNReal r

Canonical Homomorphism from Nonnegative Rationals to Extended Nonnegative Reals

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ admit a canonical homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$, where each nonnegative rational $q$ is mapped to its corresponding element in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via the inclusion $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_nnratCast theorem

(q : ℚ≥0) : ↑(q : ℝ≥0) = (q : ℝ≥0∞)

Full source

@[norm_cast]
theorem coe_nnratCast (q : ℚ≥0) : ↑(q : ℝ≥0) = (q : ℝ≥0∞) := rfl

Compatibility of Inclusions: $\uparrow(q : \mathbb{R}_{\geq 0}) = (q : \mathbb{R}_{\geq 0} \cup \{\infty\})$ for Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the canonical inclusion of $q$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via the nonnegative real numbers $\mathbb{R}_{\geq 0}$ coincides with the direct inclusion of $q$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$. In other words, $\uparrow(q : \mathbb{R}_{\geq 0}) = (q : \mathbb{R}_{\geq 0} \cup \{\infty\})$.

ENNReal.toNNReal definition

: ℝ≥0∞ → ℝ≥0

Full source

/-- `toNNReal x` returns `x` if it is real, otherwise 0. -/
protected def toNNReal : ℝ≥0∞ → ℝ≥0 := WithTop.untopD 0

Conversion from extended nonnegative reals to nonnegative reals

Informal description

The function maps an extended nonnegative real number $ x $ to its underlying nonnegative real part if $ x $ is finite, and returns $ 0 $ if $ x $ is infinity ($\infty$).

ENNReal.toReal definition

(a : ℝ≥0∞) : Real

Full source

/-- `toReal x` returns `x` if it is real, `0` otherwise. -/
protected def toReal (a : ℝ≥0∞) : Real := a.toNNReal

Conversion from extended nonnegative reals to reals

Informal description

The function maps an extended nonnegative real number $ x $ to its underlying real part if $ x $ is finite (i.e., $ x \in \mathbb{R}_{\geq 0} $), and returns $ 0 $ if $ x $ is infinity ($\infty$).

ENNReal.ofReal definition

(r : Real) : ℝ≥0∞

Full source

/-- `ofReal x` returns `x` if it is nonnegative, `0` otherwise. -/
protected def ofReal (r : Real) : ℝ≥0∞ := r.toNNReal

Extended nonnegative real embedding of a real number

Informal description

The function maps a real number $ x $ to the extended nonnegative real number obtained by taking the nonnegative part of $ x $, i.e., $ \max(x, 0) $. If $ x $ is negative, it returns $ 0 $.

ENNReal.toNNReal_coe theorem

(r : ℝ≥0) : (r : ℝ≥0∞).toNNReal = r

Full source

@[simp, norm_cast] lemma toNNReal_coe (r : ℝ≥0) : (r : ℝ≥0∞).toNNReal = r := rfl

Preservation of Nonnegative Real Numbers under Conversion to Extended Reals and Back

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the conversion of $r$ to an extended nonnegative real number and back to a nonnegative real number via `ENNReal.toNNReal` yields $r$ again, i.e., $\text{toNNReal}(r) = r$.

ENNReal.coe_toNNReal theorem

: ∀ {a : ℝ≥0∞}, a ≠ ∞ → ↑a.toNNReal = a

Full source

@[simp]
theorem coe_toNNReal : ∀ {a : ℝ≥0∞}, a ≠ ∞ → ↑a.toNNReal = a
  | ofNNReal _, _ => rfl
  | ⊤, h => (h rfl).elim

Canonical Injection of Nonnegative Real Part Equals Original Value for Finite Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \neq \infty$, the canonical injection of its nonnegative real part equals $a$, i.e., $\text{toNNReal}(a) = a$.

ENNReal.coe_comp_toNNReal_comp theorem

 {ι : Type*} {f : ι → ℝ≥0∞} (hf : ∀ x, f x ≠ ∞) : (fun (x : ℝ≥0) => (x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f

Full source

@[simp]
theorem coe_comp_toNNReal_comp {ι : Type*} {f : ι → ℝ≥0∞} (hf : ∀ x, f x ≠ ∞) :
    (fun (x : ℝ≥0) => (x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f := by
  ext x
  simp [coe_toNNReal (hf x)]

Commutativity of Conversion and Injection for Finite Extended Nonnegative Reals

Informal description

For any type $\iota$ and any function $f \colon \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f(x) \neq \infty$ for all $x \in \iota$, the composition of the canonical injection $\mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ with the conversion function $\text{toNNReal} \colon \mathbb{R}_{\geq 0} \cup \{\infty\} \to \mathbb{R}_{\geq 0}$ and with $f$ equals $f$ itself. In other words, the diagram \[ \iota \xrightarrow{f} \mathbb{R}_{\geq 0} \cup \{\infty\} \xrightarrow{\text{toNNReal}} \mathbb{R}_{\geq 0} \xrightarrow{\text{coe}} \mathbb{R}_{\geq 0} \cup \{\infty\} \] commutes when $f$ takes only finite values.

ENNReal.ofReal_toReal theorem

{a : ℝ≥0∞} (h : a ≠ ∞) : ENNReal.ofReal a.toReal = a

Full source

@[simp]
theorem ofReal_toReal {a : ℝ≥0∞} (h : a ≠ ∞) : ENNReal.ofReal a.toReal = a := by
  simp [ENNReal.toReal, ENNReal.ofReal, h]

Embedding of Real Part Preserves Finite Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \neq \infty$, the embedding of its real part equals $a$, i.e., $\text{ofReal}(\text{toReal}(a)) = a$.

ENNReal.toReal_ofReal theorem

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

Full source

@[simp]
theorem toReal_ofReal {r : ℝ} (h : 0 ≤ r) : (ENNReal.ofReal r).toReal = r :=
  max_eq_left h

Compatibility of `ofReal` and `toReal` for nonnegative reals

Informal description

For any real number $r$ such that $r \geq 0$, the composition of the extended nonnegative real embedding `ENNReal.ofReal` followed by the conversion to real numbers `ENNReal.toReal` yields the original value, i.e., $\text{toReal}(\text{ofReal}(r)) = r$.

ENNReal.toReal_ofReal' theorem

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

Full source

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

Conversion of Extended Nonnegative Real Embedding: $\text{toReal}(\text{ofReal}(r)) = \max(r, 0)$

Informal description

For any real number $r$, the conversion of the extended nonnegative real embedding of $r$ back to a real number equals the maximum of $r$ and $0$, i.e., $\text{toReal}(\text{ofReal}(r)) = \max(r, 0)$.

ENNReal.coe_toNNReal_le_self theorem

: ∀ {a : ℝ≥0∞}, ↑a.toNNReal ≤ a

Full source

theorem coe_toNNReal_le_self : ∀ {a : ℝ≥0∞}, ↑a.toNNReal ≤ a
  | ofNNReal r => by rw [toNNReal_coe]
  | ⊤ => le_top

Nonnegative Real Part is a Lower Bound in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the canonical embedding of its nonnegative real part (obtained via `toNNReal`) is less than or equal to $a$ itself, i.e., $\text{toNNReal}(a) \leq a$.

ENNReal.coe_nnreal_eq theorem

(r : ℝ≥0) : (r : ℝ≥0∞) = ENNReal.ofReal r

Full source

theorem coe_nnreal_eq (r : ℝ≥0) : (r : ℝ≥0∞) = ENNReal.ofReal r := by
  rw [ENNReal.ofReal, Real.toNNReal_coe]

Equality of Canonical Embedding and Nonnegative Part in Extended Nonnegative Reals

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical embedding of $r$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the extended nonnegative real number obtained by taking the nonnegative part of $r$, i.e., $(r : \mathbb{R}_{\geq 0} \cup \{\infty\}) = \text{ENNReal.ofReal}(r)$.

ENNReal.ofReal_eq_coe_nnreal theorem

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

Full source

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

Equality of Extended Real Embedding and Nonnegative Real Embedding for Nonnegative Reals

Informal description

For any real number $x$ such that $x \geq 0$, the extended nonnegative real number obtained via `ENNReal.ofReal x` is equal to the canonical embedding of the nonnegative real number $\langle x, h\rangle$ (where $h$ is the proof that $x \geq 0$) into the extended nonnegative reals.

ENNReal.ofNNReal_toNNReal theorem

(x : ℝ) : (Real.toNNReal x : ℝ≥0∞) = ENNReal.ofReal x

Full source

theorem ofNNReal_toNNReal (x : ℝ) : (Real.toNNReal x : ℝ≥0∞) = ENNReal.ofReal x := rfl

Equality of Nonnegative Part Inclusion and Extended Real Embedding

Informal description

For any real number $x$, the canonical embedding of the nonnegative part of $x$ (i.e., $\max(x, 0)$) into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the extended nonnegative real number obtained by applying the `ENNReal.ofReal` function to $x$. In other words, if $r = \max(x, 0)$ is the nonnegative part of $x$, then the inclusion of $r$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals $\text{ENNReal.ofReal}(x)$.

ENNReal.ofReal_coe_nnreal theorem

: ENNReal.ofReal p = p

Full source

@[simp] theorem ofReal_coe_nnreal : ENNReal.ofReal p = p := (coe_nnreal_eq p).symm

Embedding of Nonnegative Reals Preserves Identity: $\text{ENNReal.ofReal}(p) = p$

Informal description

For any nonnegative real number $p \in \mathbb{R}_{\geq 0}$, the extended nonnegative real number obtained by applying the `ENNReal.ofReal` function to $p$ is equal to $p$ itself, i.e., $\text{ENNReal.ofReal}(p) = p$.

ENNReal.coe_zero theorem

: ↑(0 : ℝ≥0) = (0 : ℝ≥0∞)

Full source

@[simp, norm_cast] theorem coe_zero : ↑(0 : ℝ≥0) = (0 : ℝ≥0∞) := rfl

Inclusion Preserves Zero in Extended Nonnegative Reals

Informal description

The canonical inclusion map from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ maps the zero element $0 \in \mathbb{R}_{\geq 0}$ to the zero element $0 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$. In other words, $\overline{0} = 0$ where $\overline{\cdot}$ denotes the inclusion map.

ENNReal.coe_one theorem

: ↑(1 : ℝ≥0) = (1 : ℝ≥0∞)

Full source

@[simp, norm_cast] theorem coe_one : ↑(1 : ℝ≥0) = (1 : ℝ≥0∞) := rfl

Inclusion Preserves One in Extended Nonnegative Reals

Informal description

The canonical inclusion map from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ maps the multiplicative identity element $1 \in \mathbb{R}_{\geq 0}$ to the multiplicative identity element $1 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$. In other words, $\overline{1} = 1$ where $\overline{\cdot}$ denotes the inclusion map.

ENNReal.toReal_nonneg theorem

{a : ℝ≥0∞} : 0 ≤ a.toReal

Full source

@[simp] theorem toReal_nonneg {a : ℝ≥0∞} : 0 ≤ a.toReal := a.toNNReal.2

Nonnegativity of Extended Nonnegative Real Conversion to Real Numbers

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real number obtained by applying the conversion function $\mathrm{toReal}$ to $a$ is nonnegative, i.e., $0 \leq \mathrm{toReal}(a)$.

ENNReal.coe_toNNReal_eq_toReal theorem

(z : ℝ≥0∞) : (z.toNNReal : ℝ) = z.toReal

Full source

@[norm_cast] theorem coe_toNNReal_eq_toReal (z : ℝ≥0∞) : (z.toNNReal : ℝ) = z.toReal := rfl

Compatibility of Conversions: $\overline{\text{toNNReal}(z)} = \text{toReal}(z)$ for $z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

For any extended nonnegative real number $z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real number obtained by first converting $z$ to a nonnegative real number (via `toNNReal`) and then including it in the real numbers (via the canonical inclusion) is equal to the direct conversion of $z$ to a real number (via `toReal`). In other words, $\overline{z_{\text{NN}}} = z_{\mathbb{R}}$, where $z_{\text{NN}} = \text{toNNReal}(z)$ and $z_{\mathbb{R}} = \text{toReal}(z)$.

ENNReal.toNNReal_toReal_eq theorem

(z : ℝ≥0∞) : z.toReal.toNNReal = z.toNNReal

Full source

@[simp] theorem toNNReal_toReal_eq (z : ℝ≥0∞) : z.toReal.toNNReal = z.toNNReal := by
  ext; simp [coe_toNNReal_eq_toReal]

Compatibility of Conversions: $\text{toNNReal} \circ \text{toReal} = \text{toNNReal}$ on Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $z \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the composition of the conversion to real numbers followed by the conversion back to nonnegative real numbers equals the direct conversion to nonnegative real numbers, i.e., $\text{toNNReal}(\text{toReal}(z)) = \text{toNNReal}(z)$.

ENNReal.toNNReal_top theorem

: ∞.toNNReal = 0

Full source

@[simp] theorem toNNReal_top : ∞.toNNReal = 0 := rfl

Conversion of Infinity to Zero in Extended Nonnegative Reals

Informal description

The conversion of the extended nonnegative real number $\infty$ to a nonnegative real number yields $0$, i.e., $\text{toNNReal}(\infty) = 0$.

ENNReal.toReal_top theorem

: ∞.toReal = 0

Full source

@[simp] theorem toReal_top : ∞.toReal = 0 := rfl

Conversion of Infinity to Zero in Extended Nonnegative Reals: $\text{toReal}(\infty) = 0$

Informal description

The conversion of the extended nonnegative real number $\infty$ to a real number yields $0$, i.e., $\text{toReal}(\infty) = 0$.

ENNReal.toReal_one theorem

: (1 : ℝ≥0∞).toReal = 1

Full source

@[simp] theorem toReal_one : (1 : ℝ≥0∞).toReal = 1 := rfl

Conversion of One in Extended Nonnegative Reals: $\text{toReal}(1) = 1$

Informal description

The conversion of the extended nonnegative real number $1$ to a real number yields $1$, i.e., $\text{toReal}(1) = 1$.

ENNReal.toNNReal_one theorem

: (1 : ℝ≥0∞).toNNReal = 1

Full source

@[simp] theorem toNNReal_one : (1 : ℝ≥0∞).toNNReal = 1 := rfl

Conversion of One in Extended Nonnegative Reals: $\text{toNNReal}(1) = 1$

Informal description

The conversion of the extended nonnegative real number $1$ to a nonnegative real number yields $1$, i.e., $\text{toNNReal}(1) = 1$.

ENNReal.coe_toReal theorem

(r : ℝ≥0) : (r : ℝ≥0∞).toReal = r

Full source

@[simp] theorem coe_toReal (r : ℝ≥0) : (r : ℝ≥0∞).toReal = r := rfl

Preservation of Value in Conversion: $\text{toReal}(r) = r$ for $r \in \mathbb{R}_{\geq 0}$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the conversion of $r$ to an extended nonnegative real number and then back to a real number via `toReal` yields $r$ itself, i.e., $\text{toReal}(r) = r$.

ENNReal.toNNReal_zero theorem

: (0 : ℝ≥0∞).toNNReal = 0

Full source

@[simp] theorem toNNReal_zero : (0 : ℝ≥0∞).toNNReal = 0 := rfl

Conversion of Zero in Extended Nonnegative Reals: $\text{toNNReal}(0) = 0$

Informal description

The conversion of the extended nonnegative real number $0$ to a nonnegative real number yields $0$, i.e., $\text{toNNReal}(0) = 0$.

ENNReal.toReal_zero theorem

: (0 : ℝ≥0∞).toReal = 0

Full source

@[simp] theorem toReal_zero : (0 : ℝ≥0∞).toReal = 0 := rfl

Conversion of Zero in Extended Nonnegative Reals: $\text{toReal}(0) = 0$

Informal description

The conversion of the extended nonnegative real number $0$ to a real number yields $0$, i.e., $\text{toReal}(0) = 0$.

ENNReal.ofReal_zero theorem

: ENNReal.ofReal (0 : ℝ) = 0

Full source

@[simp] theorem ofReal_zero : ENNReal.ofReal (0 : ℝ) = 0 := by simp [ENNReal.ofReal]

Embedding of Zero in Extended Nonnegative Reals: $\text{ENNReal.ofReal}(0) = 0$

Informal description

The embedding of the real number $0$ into the extended nonnegative real numbers is equal to $0$, i.e., $\text{ENNReal.ofReal}(0) = 0$.

ENNReal.ofReal_one theorem

: ENNReal.ofReal (1 : ℝ) = (1 : ℝ≥0∞)

Full source

@[simp] theorem ofReal_one : ENNReal.ofReal (1 : ℝ) = (1 : ℝ≥0∞) := by simp [ENNReal.ofReal]

Embedding of One in Extended Nonnegative Reals: $\text{ENNReal.ofReal}(1) = 1$

Informal description

The embedding of the real number $1$ into the extended nonnegative real numbers is equal to the extended nonnegative real number $1$, i.e., $\text{ENNReal.ofReal}(1) = 1$.

ENNReal.ofReal_toReal_le theorem

{a : ℝ≥0∞} : ENNReal.ofReal a.toReal ≤ a

Full source

theorem ofReal_toReal_le {a : ℝ≥0∞} : ENNReal.ofReal a.toReal ≤ a :=
  if ha : a = ∞ then ha.symm ▸ le_top else le_of_eq (ofReal_toReal ha)

Embedding of Real Part is a Lower Bound for Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the embedding of its real part is less than or equal to $a$, i.e., $\text{ofReal}(\text{toReal}(a)) \leq a$.

ENNReal.forall_ennreal theorem

{p : ℝ≥0∞ → Prop} : (∀ a, p a) ↔ (∀ r : ℝ≥0, p r) ∧ p ∞

Full source

theorem forall_ennreal {p : ℝ≥0∞ → Prop} : (∀ a, p a) ↔ (∀ r : ℝ≥0, p r) ∧ p ∞ :=
  Option.forall.trans and_comm

Universal Quantification Characterization for Extended Nonnegative Reals

Informal description

For any predicate $p$ on the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the statement that $p$ holds for all $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equivalent to the conjunction of $p$ holding for all $r \in \mathbb{R}_{\geq 0}$ and $p$ holding for $\infty$.

ENNReal.forall_ne_top theorem

{p : ℝ≥0∞ → Prop} : (∀ a, a ≠ ∞ → p a) ↔ ∀ r : ℝ≥0, p r

Full source

theorem forall_ne_top {p : ℝ≥0∞ → Prop} : (∀ a, a ≠ ∞ → p a) ↔ ∀ r : ℝ≥0, p r :=
  Option.forall_ne_none

Universal Quantification over Finite Extended Nonnegative Reals is Equivalent to Quantification over Nonnegative Reals

Informal description

For any predicate $p$ on the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the statement that $p(a)$ holds for all $a \neq \infty$ is equivalent to $p(r)$ holding for all nonnegative real numbers $r \in \mathbb{R}_{\geq 0}$.

ENNReal.exists_ne_top theorem

{p : ℝ≥0∞ → Prop} : (∃ a ≠ ∞, p a) ↔ ∃ r : ℝ≥0, p r

Full source

theorem exists_ne_top {p : ℝ≥0∞ → Prop} : (∃ a ≠ ∞, p a) ↔ ∃ r : ℝ≥0, p r :=
  Option.exists_ne_none

Existence of Finite Extended Nonnegative Real Satisfying Predicate is Equivalent to Existence of Nonnegative Real Satisfying Predicate

Informal description

For any predicate $p$ on the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists an element $a \neq \infty$ such that $p(a)$ holds if and only if there exists a nonnegative real number $r \in \mathbb{R}_{\geq 0}$ such that $p(r)$ holds.

ENNReal.toNNReal_eq_zero_iff theorem

(x : ℝ≥0∞) : x.toNNReal = 0 ↔ x = 0 ∨ x = ∞

Full source

theorem toNNReal_eq_zero_iff (x : ℝ≥0∞) : x.toNNReal = 0 ↔ x = 0 ∨ x = ∞ :=
  WithTop.untopD_eq_self_iff

Characterization of Zero Conversion in Extended Nonnegative Reals: $x.\text{toNNReal} = 0 \leftrightarrow x = 0 \lor x = \infty$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $x$ to a nonnegative real number equals zero if and only if $x$ is zero or infinity, i.e., $x = 0$ or $x = \infty$.

ENNReal.toReal_eq_zero_iff theorem

(x : ℝ≥0∞) : x.toReal = 0 ↔ x = 0 ∨ x = ∞

Full source

theorem toReal_eq_zero_iff (x : ℝ≥0∞) : x.toReal = 0 ↔ x = 0 ∨ x = ∞ := by
  simp [ENNReal.toReal, toNNReal_eq_zero_iff]

Real Part of Extended Nonnegative Real is Zero if and only if Zero or Infinity

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part of $x$ is zero if and only if $x = 0$ or $x = \infty$.

ENNReal.toNNReal_ne_zero theorem

: a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞

Full source

theorem toNNReal_ne_zero : a.toNNReal ≠ 0a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞ :=
  a.toNNReal_eq_zero_iff.not.trans not_or

Nonzero Conversion Criterion for Extended Nonnegative Reals: $a.\text{toNNReal} \neq 0 \leftrightarrow a \neq 0 \land a \neq \infty$

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $a$ to a nonnegative real number is nonzero if and only if $a$ is neither zero nor infinity, i.e., $a \neq 0$ and $a \neq \infty$.

ENNReal.toReal_ne_zero theorem

: a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞

Full source

theorem toReal_ne_zero : a.toReal ≠ 0a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞ :=
  a.toReal_eq_zero_iff.not.trans not_or

Nonzero Real Part of Extended Nonnegative Real Numbers

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part of $a$ is nonzero if and only if $a$ is neither zero nor infinity, i.e., $a.\text{toReal} \neq 0 \leftrightarrow a \neq 0 \land a \neq \infty$.

ENNReal.toNNReal_eq_one_iff theorem

(x : ℝ≥0∞) : x.toNNReal = 1 ↔ x = 1

Full source

theorem toNNReal_eq_one_iff (x : ℝ≥0∞) : x.toNNReal = 1 ↔ x = 1 :=
  WithTop.untopD_eq_iff.trans <| by simp

Characterization of Extended Nonnegative Reals Equal to One via Conversion to Nonnegative Reals

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $x$ to a nonnegative real number equals $1$ if and only if $x = 1$.

ENNReal.toReal_eq_one_iff theorem

(x : ℝ≥0∞) : x.toReal = 1 ↔ x = 1

Full source

theorem toReal_eq_one_iff (x : ℝ≥0∞) : x.toReal = 1 ↔ x = 1 := by
  rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]

Characterization of Extended Nonnegative Reals Equal to One via Conversion to Reals

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $x$ to a real number equals $1$ if and only if $x = 1$.

ENNReal.toNNReal_ne_one theorem

: a.toNNReal ≠ 1 ↔ a ≠ 1

Full source

theorem toNNReal_ne_one : a.toNNReal ≠ 1a.toNNReal ≠ 1 ↔ a ≠ 1 :=
  a.toNNReal_eq_one_iff.not

Non-Equality Characterization via Conversion: $a_{\text{NNReal}} \neq 1 \leftrightarrow a \neq 1$

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $a$ to a nonnegative real number is not equal to $1$ if and only if $a \neq 1$.

ENNReal.toReal_ne_one theorem

: a.toReal ≠ 1 ↔ a ≠ 1

Full source

theorem toReal_ne_one : a.toReal ≠ 1a.toReal ≠ 1 ↔ a ≠ 1 :=
  a.toReal_eq_one_iff.not

Characterization of Non-Equality via Real Conversion: $a_{\text{real}} \neq 1 \leftrightarrow a \neq 1$

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $a$ to a real number is not equal to $1$ if and only if $a \neq 1$.

ENNReal.coe_ne_top theorem

: (r : ℝ≥0∞) ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply]
theorem coe_ne_top : (r : ℝ≥0∞) ≠ ∞ := WithTop.coe_ne_top

Embedded Nonnegative Real is Not Infinity in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ that is not equal to $\infty$, the canonical embedding of $r$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $\infty$.

ENNReal.top_ne_coe theorem

: ∞ ≠ (r : ℝ≥0∞)

Full source

@[simp] theorem top_ne_coe : ∞∞ ≠ (r : ℝ≥0∞) := WithTop.top_ne_coe

Infinity is distinct from embedded nonnegative reals in $\mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

The element $\infty$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to any embedded nonnegative real number $r \in \mathbb{R}_{\geq 0}$.

ENNReal.coe_lt_top theorem

: (r : ℝ≥0∞) < ∞

Full source

@[simp] theorem coe_lt_top : (r : ℝ≥0∞) < ∞ := WithTop.coe_lt_top r

Embedded Nonnegative Reals are Strictly Below Infinity in $\mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical embedding of $r$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is strictly less than $\infty$.

ENNReal.ofReal_ne_top theorem

{r : ℝ} : ENNReal.ofReal r ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply]
theorem ofReal_ne_top {r : ℝ} : ENNReal.ofRealENNReal.ofReal r ≠ ∞ := coe_ne_top

Embedded Real Numbers are Finite in Extended Nonnegative Reals

Informal description

For any real number $r$, the extended nonnegative real number obtained by embedding $r$ (via $\text{ENNReal.ofReal}$) is not equal to $\infty$.

ENNReal.ofReal_lt_top theorem

{r : ℝ} : ENNReal.ofReal r < ∞

Full source

@[simp] theorem ofReal_lt_top {r : ℝ} : ENNReal.ofReal r < ∞ := coe_lt_top

Embedded Real Numbers are Strictly Below Infinity in Extended Nonnegative Reals

Informal description

For any real number $r$, the extended nonnegative real number obtained by embedding $r$ (via $\text{ENNReal.ofReal}$) is strictly less than $\infty$.

ENNReal.top_ne_ofReal theorem

{r : ℝ} : ∞ ≠ ENNReal.ofReal r

Full source

@[simp] theorem top_ne_ofReal {r : ℝ} : ∞∞ ≠ ENNReal.ofReal r := top_ne_coe

Infinity is not equal to any embedded real number in $\mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

For any real number $r$, the infinity element $\infty$ in the extended nonnegative real numbers is not equal to the embedding of $r$ via $\text{ENNReal.ofReal}$.

ENNReal.ofReal_toReal_eq_iff theorem

: ENNReal.ofReal a.toReal = a ↔ a ≠ ⊤

Full source

@[simp]
theorem ofReal_toReal_eq_iff : ENNReal.ofRealENNReal.ofReal a.toReal = a ↔ a ≠ ⊤ :=
  ⟨fun h => by
    rw [← h]
    exact ofReal_ne_top, ofReal_toReal⟩

Finite Characterization via Embedding of Real Part in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the embedding of its real part equals $a$ if and only if $a$ is finite, i.e., $\text{ofReal}(\text{toReal}(a)) = a \leftrightarrow a \neq \infty$.

ENNReal.toReal_ofReal_eq_iff theorem

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

Full source

@[simp]
theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ a :=
  ⟨fun h => by
    rw [← h]
    exact toReal_nonneg, toReal_ofReal⟩

Characterization of Nonnegative Reals via `ofReal` and `toReal`

Informal description

For any real number $a$, the equality $\text{toReal}(\text{ofReal}(a)) = a$ holds if and only if $a$ is nonnegative, i.e., $a \geq 0$.

ENNReal.zero_ne_top theorem

: 0 ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply] theorem zero_ne_top : 0 ≠ ∞ := coe_ne_top

Non-equality of Zero and Infinity in Extended Nonnegative Reals

Informal description

The zero element in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $\infty$, i.e., $0 \neq \infty$.

ENNReal.top_ne_zero theorem

: ∞ ≠ 0

Full source

@[simp] theorem top_ne_zero : ∞∞ ≠ 0 := top_ne_coe

Infinity is not equal to zero in extended nonnegative reals

Informal description

The element $\infty$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $0$.

ENNReal.one_ne_top theorem

: 1 ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply] theorem one_ne_top : 1 ≠ ∞ := coe_ne_top

One is not equal to infinity in extended nonnegative reals

Informal description

The element $1$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $\infty$.

ENNReal.top_ne_one theorem

: ∞ ≠ 1

Full source

@[simp] theorem top_ne_one : ∞∞ ≠ 1 := top_ne_coe

Infinity is not equal to one in extended nonnegative reals

Informal description

The element $\infty$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $1$.

ENNReal.zero_lt_top theorem

: 0 < ∞

Full source

@[simp] theorem zero_lt_top : 0 < ∞ := coe_lt_top

Strict Inequality: $0 < \infty$ in Extended Nonnegative Reals

Informal description

In the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the element $0$ is strictly less than $\infty$.

ENNReal.coe_le_coe theorem

: (↑r : ℝ≥0∞) ≤ ↑q ↔ r ≤ q

Full source

@[simp, norm_cast] theorem coe_le_coe : (↑r : ℝ≥0∞) ≤ ↑q ↔ r ≤ q := WithTop.coe_le_coe

Order Preservation in Extended Nonnegative Reals via Injection

Informal description

For any two nonnegative real numbers $r$ and $q$, the inequality $r \leq q$ holds in $\mathbb{R}_{\geq 0}$ if and only if the inequality $(r : \mathbb{R}_{\geq 0} \cup \{\infty\}) \leq (q : \mathbb{R}_{\geq 0} \cup \{\infty\})$ holds in the extended nonnegative real numbers.

ENNReal.coe_lt_coe theorem

: (↑r : ℝ≥0∞) < ↑q ↔ r < q

Full source

@[simp, norm_cast] theorem coe_lt_coe : (↑r : ℝ≥0∞) < ↑q ↔ r < q := WithTop.coe_lt_coe

Preservation of Strict Inequality under Inclusion into Extended Nonnegative Reals

Informal description

For any two nonnegative real numbers $r$ and $q$, the inequality $r < q$ holds in $\mathbb{R}_{\geq 0}$ if and only if the inequality $\overline{r} < \overline{q}$ holds in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, where $\overline{r}$ and $\overline{q}$ denote the canonical inclusions of $r$ and $q$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_mono theorem

: Monotone ofNNReal

Full source

theorem coe_mono : Monotone ofNNReal := fun _ _ => coe_le_coe.2

Monotonicity of Inclusion from Nonnegative Reals to Extended Nonnegative Reals

Informal description

The canonical inclusion map from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is monotone. That is, for any $r, q \in \mathbb{R}_{\geq 0}$, if $r \leq q$, then $\overline{r} \leq \overline{q}$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, where $\overline{r}$ and $\overline{q}$ denote the inclusions of $r$ and $q$ respectively.

ENNReal.coe_strictMono theorem

: StrictMono ofNNReal

Full source

theorem coe_strictMono : StrictMono ofNNReal := fun _ _ => coe_lt_coe.2

Strict Monotonicity of Inclusion from Nonnegative Reals to Extended Nonnegative Reals

Informal description

The canonical inclusion map from the nonnegative real numbers $\mathbb{R}_{\geq 0}$ to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is strictly monotone. That is, for any $r, q \in \mathbb{R}_{\geq 0}$, if $r < q$ then $\overline{r} < \overline{q}$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_eq_zero theorem

: (↑r : ℝ≥0∞) = 0 ↔ r = 0

Full source

@[simp, norm_cast] theorem coe_eq_zero : (↑r : ℝ≥0∞) = 0 ↔ r = 0 := coe_inj

Inclusion of Nonnegative Reals Preserves Zero: $\uparrow r = 0 \leftrightarrow r = 0$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion of $r$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals zero if and only if $r = 0$. In other words, $\uparrow r = 0 \leftrightarrow r = 0$.

ENNReal.zero_eq_coe theorem

: 0 = (↑r : ℝ≥0∞) ↔ 0 = r

Full source

@[simp, norm_cast] theorem zero_eq_coe : 0 = (↑r : ℝ≥0∞) ↔ 0 = r := coe_inj

Zero Equals Injection of Nonnegative Real if and only if Zero Equals Real

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the equality $0 = \uparrow r$ holds in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $0 = r$ in $\mathbb{R}_{\geq 0}$.

ENNReal.coe_eq_one theorem

: (↑r : ℝ≥0∞) = 1 ↔ r = 1

Full source

@[simp, norm_cast] theorem coe_eq_one : (↑r : ℝ≥0∞) = 1 ↔ r = 1 := coe_inj

Inclusion of Nonnegative Reals Preserves One

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion of $r$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals $1$ if and only if $r = 1$. In other words, $\uparrow r = 1 \leftrightarrow r = 1$.

ENNReal.one_eq_coe theorem

: 1 = (↑r : ℝ≥0∞) ↔ 1 = r

Full source

@[simp, norm_cast] theorem one_eq_coe : 1 = (↑r : ℝ≥0∞) ↔ 1 = r := coe_inj

Equality of One with Extended Nonnegative Real Inclusion: $1 = \uparrow r \leftrightarrow 1 = r$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the extended nonnegative real number $1$ is equal to the canonical inclusion of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $1 = r$ in $\mathbb{R}_{\geq 0}$.

ENNReal.coe_pos theorem

: 0 < (r : ℝ≥0∞) ↔ 0 < r

Full source

@[simp, norm_cast] theorem coe_pos : 0 < (r : ℝ≥0∞) ↔ 0 < r := coe_lt_coe

Positivity Preservation in Extended Nonnegative Reals: $0 < \overline{r} \leftrightarrow 0 < r$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion $\overline{r} \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfies $0 < \overline{r}$ if and only if $0 < r$ in $\mathbb{R}_{\geq 0}$.

ENNReal.coe_ne_zero theorem

: (r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0

Full source

theorem coe_ne_zero : (r : ℝ≥0∞) ≠ 0(r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0 := coe_eq_zero.not

Nonzero Preservation in Extended Nonnegative Reals: $\uparrow r \neq 0 \leftrightarrow r \neq 0$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion of $r$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is nonzero if and only if $r$ is nonzero. In other words, $\uparrow r \neq 0 \leftrightarrow r \neq 0$.

ENNReal.coe_ne_one theorem

: (r : ℝ≥0∞) ≠ 1 ↔ r ≠ 1

Full source

lemma coe_ne_one : (r : ℝ≥0∞) ≠ 1(r : ℝ≥0∞) ≠ 1 ↔ r ≠ 1 := coe_eq_one.not

Inclusion of Nonnegative Reals Preserves Non-One Condition

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the canonical inclusion of $r$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $1$ if and only if $r \neq 1$. In other words, $\uparrow r \neq 1 \leftrightarrow r \neq 1$.

ENNReal.coe_add theorem

(x y : ℝ≥0) : (↑(x + y) : ℝ≥0∞) = x + y

Full source

@[simp, norm_cast] lemma coe_add (x y : ℝ≥0) : (↑(x + y) : ℝ≥0∞) = x + y := rfl

Inclusion Preserves Addition in Extended Nonnegative Reals

Informal description

For any nonnegative real numbers $x$ and $y$, the canonical inclusion of their sum into the extended nonnegative real numbers equals the sum of their inclusions, i.e., $\overline{x + y} = \overline{x} + \overline{y}$.

ENNReal.coe_mul theorem

(x y : ℝ≥0) : (↑(x * y) : ℝ≥0∞) = x * y

Full source

@[simp, norm_cast] lemma coe_mul (x y : ℝ≥0) : (↑(x * y) : ℝ≥0∞) = x * y := rfl

Inclusion Preserves Multiplication in Extended Nonnegative Reals

Informal description

For any nonnegative real numbers $x$ and $y$, the canonical inclusion of their product into the extended nonnegative real numbers equals the product of their inclusions, i.e., $\overline{x \cdot y} = \overline{x} \cdot \overline{y}$.

ENNReal.coe_nsmul theorem

(n : ℕ) (x : ℝ≥0) : (↑(n • x) : ℝ≥0∞) = n • x

Full source

@[norm_cast] lemma coe_nsmul (n : ℕ) (x : ℝ≥0) : (↑(n • x) : ℝ≥0∞) = n • x := rfl

Scalar Multiplication Commutes with Inclusion into Extended Nonnegative Reals

Informal description

For any natural number $n$ and any nonnegative real number $x$, the canonical injection of the scalar multiple $n \cdot x$ into the extended nonnegative real numbers equals the scalar multiple of the injection of $x$ by $n$, i.e., $\overline{n \cdot x} = n \cdot \overline{x}$.

ENNReal.coe_pow theorem

(x : ℝ≥0) (n : ℕ) : (↑(x ^ n) : ℝ≥0∞) = x ^ n

Full source

@[simp, norm_cast] lemma coe_pow (x : ℝ≥0) (n : ℕ) : (↑(x ^ n) : ℝ≥0∞) = x ^ n := rfl

Power Preservation under Inclusion into Extended Nonnegative Reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$ and any natural number $n \in \mathbb{N}$, the canonical inclusion of $x^n$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the $n$-th power of the inclusion of $x$, i.e., $\overline{x^n} = (\overline{x})^n$.

ENNReal.coe_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ≥0) : ℝ≥0∞) = ofNat(n)

Full source

@[simp, norm_cast]
theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℝ≥0) : ℝ≥0∞) = ofNat(n) := rfl

Preservation of Numerals ≥ 2 under Inclusion into Extended Nonnegative Reals

Informal description

For any natural number $n \geq 2$, the canonical inclusion of the numeral $n$ from nonnegative real numbers $\mathbb{R}_{\geq 0}$ to extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ preserves the value, i.e., $\overline{n} = n$.

ENNReal.coe_two theorem

: ((2 : ℝ≥0) : ℝ≥0∞) = 2

Full source

theorem coe_two : ((2 : ℝ≥0) : ℝ≥0∞) = 2 := rfl

Preservation of Two under Inclusion into Extended Nonnegative Reals

Informal description

The canonical inclusion of the nonnegative real number $2$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ preserves the value, i.e., $\overline{2} = 2$.

ENNReal.toNNReal_eq_toNNReal_iff theorem

(x y : ℝ≥0∞) : x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

Full source

theorem toNNReal_eq_toNNReal_iff (x y : ℝ≥0∞) :
    x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 :=
  WithTop.untopD_eq_untopD_iff

Equivalence of Projection Equality and Special Cases in Extended Nonnegative Reals

Informal description

For any extended nonnegative real numbers $x$ and $y$, the equality of their projections to nonnegative real numbers, $\mathrm{toNNReal}(x) = \mathrm{toNNReal}(y)$, holds if and only if either $x = y$, or $x = 0$ and $y = \infty$, or $x = \infty$ and $y = 0$.

ENNReal.toReal_eq_toReal_iff theorem

(x y : ℝ≥0∞) : x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

Full source

theorem toReal_eq_toReal_iff (x y : ℝ≥0∞) :
    x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 := by
  simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

Equality of Extended Nonnegative Reals via Real Conversion

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the equality $x.\text{toReal} = y.\text{toReal}$ holds if and only if either $x = y$, or $x = 0$ and $y = \infty$, or $x = \infty$ and $y = 0$.

ENNReal.toNNReal_eq_toNNReal_iff' theorem

{x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toNNReal = y.toNNReal ↔ x = y

Full source

theorem toNNReal_eq_toNNReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
    x.toNNReal = y.toNNReal ↔ x = y := by
  simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]

Finite Extended Nonnegative Reals Have Equal Projections if and only if They Are Equal

Informal description

For any extended nonnegative real numbers $x$ and $y$ such that $x \neq \infty$ and $y \neq \infty$, the equality $\mathrm{toNNReal}(x) = \mathrm{toNNReal}(y)$ holds if and only if $x = y$.

ENNReal.toReal_eq_toReal_iff' theorem

{x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toReal = y.toReal ↔ x = y

Full source

theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
    x.toReal = y.toReal ↔ x = y := by
  simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff' hx hy]

Finite Extended Nonnegative Reals Have Equal Real Conversions if and only if They Are Equal

Informal description

For any extended nonnegative real numbers $x$ and $y$ such that $x \neq \infty$ and $y \neq \infty$, the equality $x.\mathrm{toReal} = y.\mathrm{toReal}$ holds if and only if $x = y$.

ENNReal.one_lt_two theorem

: (1 : ℝ≥0∞) < 2

Full source

theorem one_lt_two : (1 : ℝ≥0∞) < 2 := Nat.one_lt_ofNat

$1 < 2$ in extended nonnegative reals

Informal description

In the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $1 < 2$ holds.

fact_one_le_one_ennreal instance

: Fact ((1 : ℝ≥0∞) ≤ 1)

Full source

/-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `Fact` for use with `Lp` spaces. -/
instance _root_.fact_one_le_one_ennreal : Fact ((1 : ℝ≥0∞) ≤ 1) :=
  ⟨le_rfl⟩

One is Less Than or Equal to One in Extended Nonnegative Reals

Informal description

The extended nonnegative real number $1$ is less than or equal to itself, i.e., $1 \leq 1$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

fact_one_le_two_ennreal instance

: Fact ((1 : ℝ≥0∞) ≤ 2)

Full source

/-- `(1 : ℝ≥0∞) ≤ 2`, recorded as a `Fact` for use with `Lp` spaces. -/
instance _root_.fact_one_le_two_ennreal : Fact ((1 : ℝ≥0∞) ≤ 2) :=
  ⟨one_le_two⟩

One is Less Than or Equal to Two in Extended Nonnegative Reals

Informal description

The extended nonnegative real number $1$ is less than or equal to $2$, i.e., $1 \leq 2$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

fact_one_le_top_ennreal instance

: Fact ((1 : ℝ≥0∞) ≤ ∞)

Full source

/-- `(1 : ℝ≥0∞) ≤ ∞`, recorded as a `Fact` for use with `Lp` spaces. -/
instance _root_.fact_one_le_top_ennreal : Fact ((1 : ℝ≥0∞) ≤ ∞) :=
  ⟨le_top⟩

One is Less Than or Equal to Infinity in Extended Nonnegative Reals

Informal description

The extended nonnegative real number $1$ is less than or equal to $\infty$.

ENNReal.neTopEquivNNReal definition

: {a | a ≠ ∞} ≃ ℝ≥0

Full source

/-- The set of numbers in `ℝ≥0∞` that are not equal to `∞` is equivalent to `ℝ≥0`. -/
def neTopEquivNNReal : { a | a ≠ ∞ }{ a | a ≠ ∞ } ≃ ℝ≥0 where
  toFun x := ENNReal.toNNReal x
  invFun x := ⟨x, coe_ne_top⟩
  left_inv := fun x => Subtype.eq <| coe_toNNReal x.2
  right_inv := toNNReal_coe

Equivalence between finite extended nonnegative reals and nonnegative reals

Informal description

The equivalence between the set $\{a \in \mathbb{R}_{\geq 0} \cup \{\infty\} \mid a \neq \infty\}$ and the nonnegative real numbers $\mathbb{R}_{\geq 0}$, given by the function that maps an extended nonnegative real number $a \neq \infty$ to its underlying nonnegative real part via `ENNReal.toNNReal`, and the inverse function that injects a nonnegative real number into the extended nonnegative reals via `ENNReal.ofNNReal`.

ENNReal.cinfi_ne_top theorem

[InfSet α] (f : ℝ≥0∞ → α) : ⨅ x : { x // x ≠ ∞ }, f x = ⨅ x : ℝ≥0, f x

Full source

theorem cinfi_ne_top [InfSet α] (f : ℝ≥0∞ → α) : ⨅ x : { x // x ≠ ∞ }, f x = ⨅ x : ℝ≥0, f x :=
  Eq.symm <| neTopEquivNNReal.symm.surjective.iInf_congr _ fun _ => rfl

Infimum Equality for Finite Extended Nonnegative Reals and Nonnegative Reals

Informal description

For any infimum structure $\alpha$ and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the infimum of $f$ over all finite extended nonnegative real numbers (i.e., $x \neq \infty$) is equal to the infimum of $f$ over all nonnegative real numbers. In symbols: \[ \bigsqcap_{x \in \{a \mid a \neq \infty\}} f(x) = \bigsqcap_{x \in \mathbb{R}_{\geq 0}} f(x). \]

ENNReal.iInf_ne_top theorem

[CompleteLattice α] (f : ℝ≥0∞ → α) : ⨅ (x) (_ : x ≠ ∞), f x = ⨅ x : ℝ≥0, f x

Full source

theorem iInf_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) :
    ⨅ (x) (_ : x ≠ ∞), f x = ⨅ x : ℝ≥0, f x := by rw [iInf_subtype', cinfi_ne_top]

Infimum Equality for Finite Extended Nonnegative Reals and Nonnegative Reals

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the infimum of $f$ over all finite extended nonnegative real numbers (i.e., $x \neq \infty$) is equal to the infimum of $f$ over all nonnegative real numbers. In symbols: \[ \inf_{x \neq \infty} f(x) = \inf_{x \in \mathbb{R}_{\geq 0}} f(x). \]

ENNReal.csupr_ne_top theorem

[SupSet α] (f : ℝ≥0∞ → α) : ⨆ x : { x // x ≠ ∞ }, f x = ⨆ x : ℝ≥0, f x

Full source

theorem csupr_ne_top [SupSet α] (f : ℝ≥0∞ → α) : ⨆ x : { x // x ≠ ∞ }, f x = ⨆ x : ℝ≥0, f x :=
  @cinfi_ne_top αᵒᵈ _ _

Supremum Equality for Finite Extended Nonnegative Reals and Nonnegative Reals

Informal description

For any type $\alpha$ with a supremum structure and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the supremum of $f$ over all finite extended nonnegative real numbers (i.e., $x \neq \infty$) is equal to the supremum of $f$ over all nonnegative real numbers. In symbols: \[ \bigsqcup_{x \in \{a \mid a \neq \infty\}} f(x) = \bigsqcup_{x \in \mathbb{R}_{\geq 0}} f(x). \]

ENNReal.iSup_ne_top theorem

[CompleteLattice α] (f : ℝ≥0∞ → α) : ⨆ (x) (_ : x ≠ ∞), f x = ⨆ x : ℝ≥0, f x

Full source

theorem iSup_ne_top [CompleteLattice α] (f : ℝ≥0∞ → α) :
    ⨆ (x) (_ : x ≠ ∞), f x = ⨆ x : ℝ≥0, f x :=
  @iInf_ne_top αᵒᵈ _ _

Supremum Equality for Finite Extended Nonnegative Reals and Nonnegative Reals

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the supremum of $f$ over all finite extended nonnegative real numbers (i.e., $x \neq \infty$) is equal to the supremum of $f$ over all nonnegative real numbers. In symbols: \[ \sup_{x \neq \infty} f(x) = \sup_{x \in \mathbb{R}_{\geq 0}} f(x). \]

ENNReal.iInf_ennreal theorem

{α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} : ⨅ n, f n = (⨅ n : ℝ≥0, f n) ⊓ f ∞

Full source

theorem iInf_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} :
    ⨅ n, f n = (⨅ n : ℝ≥0, f n) ⊓ f ∞ :=
  (iInf_option f).trans (inf_comm _ _)

Infimum Decomposition for Extended Nonnegative Reals: $\bigsqcap_{n \in \mathbb{R}_{\geq 0} \cup \{\infty\}} f(n) = (\bigsqcap_{n \in \mathbb{R}_{\geq 0}} f(n)) \sqcap f(\infty)$

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the infimum of $f$ over all extended nonnegative real numbers is equal to the infimum of $f$ over all nonnegative real numbers $\mathbb{R}_{\geq 0}$ meet (infimum) with $f(\infty)$. In symbols: \[ \bigsqcap_{n \in \mathbb{R}_{\geq 0} \cup \{\infty\}} f(n) = \left(\bigsqcap_{n \in \mathbb{R}_{\geq 0}} f(n)\right) \sqcap f(\infty). \]

ENNReal.iSup_ennreal theorem

{α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} : ⨆ n, f n = (⨆ n : ℝ≥0, f n) ⊔ f ∞

Full source

theorem iSup_ennreal {α : Type*} [CompleteLattice α] {f : ℝ≥0∞ → α} :
    ⨆ n, f n = (⨆ n : ℝ≥0, f n) ⊔ f ∞ :=
  @iInf_ennreal αᵒᵈ _ _

Supremum Decomposition for Extended Nonnegative Reals: $\bigsqcup_{n \in \mathbb{R}_{\geq 0} \cup \{\infty\}} f(n) = (\bigsqcup_{n \in \mathbb{R}_{\geq 0}} f(n)) \sqcup f(\infty)$

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{R}_{\geq 0} \cup \{\infty\} \to \alpha$, the supremum of $f$ over all extended nonnegative real numbers is equal to the supremum of $f$ over all nonnegative real numbers $\mathbb{R}_{\geq 0}$ join (supremum) with $f(\infty)$. In symbols: \[ \bigsqcup_{n \in \mathbb{R}_{\geq 0} \cup \{\infty\}} f(n) = \left(\bigsqcup_{n \in \mathbb{R}_{\geq 0}} f(n)\right) \sqcup f(\infty). \]

ENNReal.ofNNRealHom definition

: ℝ≥0 →+* ℝ≥0∞

Full source

/-- Coercion `ℝ≥0 → ℝ≥0∞` as a `RingHom`. -/
def ofNNRealHom : ℝ≥0ℝ≥0 →+* ℝ≥0∞ where
  toFun := some
  map_one' := coe_one
  map_mul' _ _ := coe_mul _ _
  map_zero' := coe_zero
  map_add' _ _ := coe_add _ _

Inclusion homomorphism from nonnegative reals to extended nonnegative reals

Informal description

The ring homomorphism that embeds the nonnegative real numbers $\mathbb{R}_{\geq 0}$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ by mapping each $x \in \mathbb{R}_{\geq 0}$ to itself (as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$). This homomorphism preserves the additive and multiplicative structures, sending $1$ to $1$, $0$ to $0$, and satisfying $\overline{x + y} = \overline{x} + \overline{y}$ and $\overline{x \cdot y} = \overline{x} \cdot \overline{y}$ for all $x, y \in \mathbb{R}_{\geq 0}$.

ENNReal.coe_ofNNRealHom theorem

: ⇑ofNNRealHom = some

Full source

@[simp] theorem coe_ofNNRealHom : ⇑ofNNRealHom = some := rfl

Inclusion Homomorphism as Canonical Embedding for Extended Nonnegative Reals

Informal description

The underlying function of the inclusion homomorphism from nonnegative real numbers to extended nonnegative real numbers is equal to the canonical embedding `some : ℝ≥0 → ℝ≥0∞`.

ENNReal.bot_eq_zero theorem

: (⊥ : ℝ≥0∞) = 0

Full source

theorem bot_eq_zero : (⊥ : ℝ≥0∞) = 0 := rfl

Bottom Element of Extended Nonnegative Reals is Zero

Informal description

The bottom element of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to $0$, i.e., $\bot = 0$.

ENNReal.not_top_le_coe theorem

: ¬∞ ≤ ↑r

Full source

theorem not_top_le_coe : ¬∞ ≤ ↑r := WithTop.not_top_le_coe r

$\infty$ is not bounded above by any finite nonnegative real

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the extended nonnegative real number $\infty$ is not less than or equal to the canonical inclusion of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$. In other words, $\neg (\infty \leq r)$.

ENNReal.one_le_coe_iff theorem

: (1 : ℝ≥0∞) ≤ ↑r ↔ 1 ≤ r

Full source

@[simp, norm_cast]
theorem one_le_coe_iff : (1 : ℝ≥0∞) ≤ ↑r ↔ 1 ≤ r := coe_le_coe

One is less than or equal to a nonnegative real in extended reals if and only if it is in the base reals

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the extended nonnegative real number $1$ is less than or equal to the canonical inclusion of $r$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $1 \leq r$ in $\mathbb{R}_{\geq 0}$.

ENNReal.coe_le_one_iff theorem

: ↑r ≤ (1 : ℝ≥0∞) ↔ r ≤ 1

Full source

@[simp, norm_cast]
theorem coe_le_one_iff : ↑r ≤ (1 : ℝ≥0∞) ↔ r ≤ 1 := coe_le_coe

Inclusion Preserves Order with One in Extended Nonnegative Reals

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the inequality $r \leq 1$ holds if and only if the canonical inclusion of $r$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfies $(r : \mathbb{R}_{\geq 0} \cup \{\infty\}) \leq 1$.

ENNReal.coe_lt_one_iff theorem

: (↑p : ℝ≥0∞) < 1 ↔ p < 1

Full source

@[simp, norm_cast]
theorem coe_lt_one_iff : (↑p : ℝ≥0∞) < 1 ↔ p < 1 := coe_lt_coe

Strict Inequality Preservation for Inclusion of Nonnegative Reals into Extended Nonnegative Reals: $\overline{p} < 1 \leftrightarrow p < 1$

Informal description

For any nonnegative real number $p$, the inclusion $\overline{p} < 1$ holds in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $p < 1$ holds in $\mathbb{R}_{\geq 0}$.

ENNReal.one_lt_coe_iff theorem

: 1 < (↑p : ℝ≥0∞) ↔ 1 < p

Full source

@[simp, norm_cast]
theorem one_lt_coe_iff : 1 < (↑p : ℝ≥0∞) ↔ 1 < p := coe_lt_coe

One is Less Than Extended Nonnegative Real iff One is Less Than Original Real

Informal description

For any nonnegative real number $p$, the inequality $1 < p$ holds if and only if the inequality $1 < \overline{p}$ holds in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$, where $\overline{p}$ denotes the canonical inclusion of $p$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_natCast theorem

(n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n

Full source

@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n := rfl

Natural Number Inclusion in Extended Nonnegative Reals: $(n : \mathbb{R}_{\geq 0}) = n$

Informal description

For any natural number $n$, the canonical inclusion of $n$ as a nonnegative real number into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to $n$ as an extended nonnegative real number, i.e., $(n : \mathbb{R}_{\geq 0}) = n$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.ofReal_natCast theorem

(n : ℕ) : ENNReal.ofReal n = n

Full source

@[simp, norm_cast] lemma ofReal_natCast (n : ℕ) : ENNReal.ofReal n = n := by simp [ENNReal.ofReal]

Natural Number Embedding in Extended Nonnegative Reals: $\text{ENNReal.ofReal}(n) = n$

Informal description

For any natural number $n$, the extended nonnegative real number obtained by applying `ENNReal.ofReal` to $n$ is equal to $n$ itself, i.e., $\text{ENNReal.ofReal}(n) = n$.

ENNReal.ofReal_ofNat theorem

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

Full source

@[simp] theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.ofReal ofNat(n) = ofNat(n) :=
  ofReal_natCast n

Embedding of Numerals $\geq 2$ in Extended Nonnegative Reals: $\text{ENNReal.ofReal}(n) = n$

Informal description

For any natural number $n \geq 2$, the extended nonnegative real number obtained by applying $\text{ENNReal.ofReal}$ to $n$ is equal to $n$ itself, i.e., $\text{ENNReal.ofReal}(n) = n$.

ENNReal.natCast_ne_top theorem

(n : ℕ) : (n : ℝ≥0∞) ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply]
theorem natCast_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := WithTop.natCast_ne_top n

Natural Number Cast to Extended Nonnegative Reals is Finite

Informal description

For any natural number $n$, the extended nonnegative real number obtained by casting $n$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $\infty$.

ENNReal.natCast_lt_top theorem

(n : ℕ) : (n : ℝ≥0∞) < ∞

Full source

@[simp] theorem natCast_lt_top (n : ℕ) : (n : ℝ≥0∞) < ∞ := WithTop.natCast_lt_top n

Natural number cast is finite in extended nonnegative reals

Informal description

For any natural number $n$, the extended nonnegative real number obtained by casting $n$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is strictly less than $\infty$.

ENNReal.ofNat_ne_top theorem

{n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) ≠ ∞

Full source

@[simp, aesop (rule_sets := [finiteness]) safe apply]
lemma ofNat_ne_top {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n)ofNat(n) ≠ ∞ := natCast_ne_top n

Finite value of numerals $\geq 2$ in extended nonnegative reals

Informal description

For any natural number $n \geq 2$, the extended nonnegative real number obtained by interpreting $n$ as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is not equal to $\infty$.

ENNReal.ofNat_lt_top theorem

{n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) < ∞

Full source

@[simp]
lemma ofNat_lt_top {n : ℕ} [Nat.AtLeastTwo n] : ofNat(n) < ∞ := natCast_lt_top n

Finite value of numerals $\geq 2$ in extended nonnegative reals

Informal description

For any natural number $n \geq 2$, the extended nonnegative real number obtained by interpreting $n$ as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is strictly less than $\infty$.

ENNReal.top_ne_natCast theorem

(n : ℕ) : ∞ ≠ n

Full source

@[simp] theorem top_ne_natCast (n : ℕ) : ∞∞ ≠ n := WithTop.top_ne_natCast n

$\infty \neq n$ for any natural number $n$ in extended nonnegative reals

Informal description

For any natural number $n$, the extended nonnegative real number $\infty$ is not equal to the natural number $n$ considered as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.top_ne_ofNat theorem

{n : ℕ} [n.AtLeastTwo] : ∞ ≠ ofNat(n)

Full source

@[simp] theorem top_ne_ofNat {n : ℕ} [n.AtLeastTwo] : ∞∞ ≠ ofNat(n) :=
  ofNat_ne_top.symm

$\infty \neq n$ for $n \geq 2$ in extended nonnegative reals

Informal description

For any natural number $n \geq 2$, the extended nonnegative real number $\infty$ is not equal to the extended nonnegative real number obtained by interpreting $n$ as an element of $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.two_ne_top theorem

: (2 : ℝ≥0∞) ≠ ∞

Full source

@[deprecated ofNat_ne_top (since := "2025-01-21")] lemma two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top

$2 \neq \infty$ in extended nonnegative reals

Informal description

The extended nonnegative real number $2$ is not equal to $\infty$.

ENNReal.two_lt_top theorem

: (2 : ℝ≥0∞) < ∞

Full source

@[deprecated ofNat_lt_top (since := "2025-01-21")] lemma two_lt_top : (2 : ℝ≥0∞) < ∞ := coe_lt_top

$2 < \infty$ in extended nonnegative reals

Informal description

The extended nonnegative real number $2$ is strictly less than $\infty$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.one_lt_top theorem

: 1 < ∞

Full source

@[simp] theorem one_lt_top : 1 < ∞ := coe_lt_top

$1 < \infty$ in extended nonnegative reals

Informal description

The extended nonnegative real number $1$ is strictly less than $\infty$.

ENNReal.toNNReal_natCast theorem

(n : ℕ) : (n : ℝ≥0∞).toNNReal = n

Full source

@[simp, norm_cast]
theorem toNNReal_natCast (n : ℕ) : (n : ℝ≥0∞).toNNReal = n := by
  rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]

Preservation of Natural Numbers under Conversion to Extended Nonnegative Reals and Back

Informal description

For any natural number $n$, the conversion of $n$ to an extended nonnegative real number and back to a nonnegative real number via `ENNReal.toNNReal` yields $n$ again, i.e., $\text{toNNReal}(n) = n$.

ENNReal.toNNReal_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : ENNReal.toNNReal ofNat(n) = ofNat(n)

Full source

theorem toNNReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.toNNReal ofNat(n) = ofNat(n) :=
  toNNReal_natCast n

Preservation of Numerals ≥ 2 under Conversion to Extended Nonnegative Reals and Back

Informal description

For any natural number $n \geq 2$, the conversion of the extended nonnegative real number $n$ (interpreted via `OfNat`) back to a nonnegative real number via `ENNReal.toNNReal` yields $n$ again, i.e., $\text{toNNReal}(n) = n$.

ENNReal.toReal_natCast theorem

(n : ℕ) : (n : ℝ≥0∞).toReal = n

Full source

@[simp, norm_cast]
theorem toReal_natCast (n : ℕ) : (n : ℝ≥0∞).toReal = n := by
  rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]

Preservation of Natural Numbers under Conversion to Extended Nonnegative Reals and Back to Reals

Informal description

For any natural number $n$, the conversion of $n$ to an extended nonnegative real number and back to a real number via `ENNReal.toReal` yields $n$ again, i.e., $\text{toReal}(n) = n$.

ENNReal.toReal_ofNat theorem

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

Full source

@[simp] theorem toReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.toReal ofNat(n) = ofNat(n) :=
  toReal_natCast n

Preservation of Numerals ≥ 2 under Conversion to Extended Nonnegative Reals and Back to Reals

Informal description

For any natural number $n \geq 2$, the conversion of the extended nonnegative real number $n$ (interpreted via the `OfNat` instance) back to a real number via `ENNReal.toReal` yields $n$ again, i.e., $\text{toReal}(n) = n$.

ENNReal.toNNReal_natCast_eq_toNNReal theorem

(n : ℕ) : (n : ℝ≥0∞).toNNReal = (n : ℝ).toNNReal

Full source

lemma toNNReal_natCast_eq_toNNReal (n : ℕ) :
    (n : ℝ≥0∞).toNNReal = (n : ℝ).toNNReal := by
  rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]

Equality of Conversions for Natural Numbers in Extended Nonnegative Reals and Reals

Informal description

For any natural number $n$, the conversion of $n$ to an extended nonnegative real number and back to a nonnegative real number via `ENNReal.toNNReal` is equal to the direct conversion of $n$ to a nonnegative real number, i.e., $\text{toNNReal}(n) = \text{toNNReal}(n : \mathbb{R})$.

ENNReal.le_coe_iff theorem

: a ≤ ↑r ↔ ∃ p : ℝ≥0, a = p ∧ p ≤ r

Full source

theorem le_coe_iff : a ≤ ↑r ↔ ∃ p : ℝ≥0, a = p ∧ p ≤ r := WithTop.le_coe_iff

Characterization of Inequality in Extended Nonnegative Reals via Injection

Informal description

For any extended nonnegative real number $a$ and any nonnegative real number $r$, the inequality $a \leq r$ holds if and only if there exists a nonnegative real number $p$ such that $a = p$ and $p \leq r$.

ENNReal.coe_le_iff theorem

: ↑r ≤ a ↔ ∀ p : ℝ≥0, a = p → r ≤ p

Full source

theorem coe_le_iff : ↑r ≤ a ↔ ∀ p : ℝ≥0, a = p → r ≤ p := WithTop.coe_le_iff

Characterization of Inequality Between Nonnegative and Extended Nonnegative Reals

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$ and any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $r \leq a$ holds if and only if for every $p \in \mathbb{R}_{\geq 0}$ such that $a = p$, we have $r \leq p$.

ENNReal.lt_iff_exists_coe theorem

: a < b ↔ ∃ p : ℝ≥0, a = p ∧ ↑p < b

Full source

theorem lt_iff_exists_coe : a < b ↔ ∃ p : ℝ≥0, a = p ∧ ↑p < b :=
  WithTop.lt_iff_exists_coe

Characterization of Strict Inequality in Extended Nonnegative Reals via Underlying Nonnegative Real

Informal description

For any extended nonnegative real numbers $a$ and $b$, the inequality $a < b$ holds if and only if there exists a nonnegative real number $p \in \mathbb{R}_{\geq 0}$ such that $a = p$ and the inclusion of $p$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfies $\uparrow p < b$.

ENNReal.toReal_le_coe_of_le_coe theorem

{a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.toReal ≤ b

Full source

theorem toReal_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.toReal ≤ b := by
  lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
  simpa using h

Real Conversion Preserves Order: $a \leq b \Rightarrow a.\text{toReal} \leq b$ for $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}, b \in \mathbb{R}_{\geq 0}$

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any nonnegative real number $b \in \mathbb{R}_{\geq 0}$, if $a \leq b$ then the real-valued conversion of $a$ satisfies $a.\text{toReal} \leq b$.

ENNReal.max_eq_zero_iff theorem

: max a b = 0 ↔ a = 0 ∧ b = 0

Full source

@[simp] theorem max_eq_zero_iff : maxmax a b = 0 ↔ a = 0 ∧ b = 0 := max_eq_bot

Characterization of Zero Maximum in Extended Nonnegative Reals: $\max(a, b) = 0 \leftrightarrow a = 0 \land b = 0$

Informal description

For any extended nonnegative real numbers $a$ and $b$, the maximum $\max(a, b)$ equals $0$ if and only if both $a = 0$ and $b = 0$.

ENNReal.max_zero_left theorem

: max 0 a = a

Full source

theorem max_zero_left : max 0 a = a :=
  max_eq_right (zero_le a)

Maximum with Zero in Extended Nonnegative Reals: $\max(0, a) = a$

Informal description

For any extended nonnegative real number $a$, the maximum of $0$ and $a$ is equal to $a$, i.e., $\max(0, a) = a$.

ENNReal.max_zero_right theorem

: max a 0 = a

Full source

theorem max_zero_right : max a 0 = a :=
  max_eq_left (zero_le a)

Maximum with Zero in Extended Nonnegative Reals: $\max(a, 0) = a$

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the maximum of $a$ and $0$ is equal to $a$, i.e., $\max(a, 0) = a$.

ENNReal.lt_iff_exists_rat_btwn theorem

: a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ (Real.toNNReal q : ℝ≥0∞) < b

Full source

theorem lt_iff_exists_rat_btwn :
    a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ (Real.toNNReal q : ℝ≥0∞) < b :=
  ⟨fun h => by
    rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩
    rcases exists_between h with ⟨c, pc, cb⟩
    rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩
    rcases (NNReal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩
    exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩,
      fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩

Characterization of Strict Inequality in Extended Nonnegative Reals via Rational Intermediates

Informal description

For any extended nonnegative real numbers $a$ and $b$, the inequality $a < b$ holds if and only if there exists a nonnegative rational number $q \geq 0$ such that $a$ is less than the nonnegative real number obtained from $q$ (via `Real.toNNReal`), and the inclusion of this nonnegative real number in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is less than $b$.

ENNReal.lt_iff_exists_real_btwn theorem

: a < b ↔ ∃ r : ℝ, 0 ≤ r ∧ a < ENNReal.ofReal r ∧ (ENNReal.ofReal r : ℝ≥0∞) < b

Full source

theorem lt_iff_exists_real_btwn :
    a < b ↔ ∃ r : ℝ, 0 ≤ r ∧ a < ENNReal.ofReal r ∧ (ENNReal.ofReal r : ℝ≥0∞) < b :=
  ⟨fun h =>
    let ⟨q, q0, aq, qb⟩ := ENNReal.lt_iff_exists_rat_btwn.1 h
    ⟨q, Rat.cast_nonneg.2 q0, aq, qb⟩,
    fun ⟨_, _, qa, qb⟩ => lt_trans qa qb⟩

Characterization of Strict Inequality in Extended Nonnegative Reals via Intermediate Real Numbers

Informal description

For any extended nonnegative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the strict inequality $a < b$ holds if and only if there exists a nonnegative real number $r \geq 0$ such that $a$ is less than the extended nonnegative real number obtained from $r$ (via `ENNReal.ofReal`), and this extended nonnegative real number is in turn less than $b$.

ENNReal.lt_iff_exists_nnreal_btwn theorem

: a < b ↔ ∃ r : ℝ≥0, a < r ∧ (r : ℝ≥0∞) < b

Full source

theorem lt_iff_exists_nnreal_btwn : a < b ↔ ∃ r : ℝ≥0, a < r ∧ (r : ℝ≥0∞) < b :=
  WithTop.lt_iff_exists_coe_btwn

Characterization of Strict Inequality in Extended Nonnegative Reals via Intermediate Nonnegative Real

Informal description

For any two extended nonnegative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a < b$ holds if and only if there exists a nonnegative real number $r \in \mathbb{R}_{\geq 0}$ such that $a < r$ and $r < b$ when viewed in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.lt_iff_exists_add_pos_lt theorem

: a < b ↔ ∃ r : ℝ≥0, 0 < r ∧ a + r < b

Full source

theorem lt_iff_exists_add_pos_lt : a < b ↔ ∃ r : ℝ≥0, 0 < r ∧ a + r < b := by
  refine ⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩
  rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩
  lift a to ℝ≥0 using ac.ne_top
  rw [coe_lt_coe] at ac
  refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩
  rwa [← coe_add, add_tsub_cancel_of_le ac.le]

Characterization of Strict Inequality in Extended Nonnegative Reals via Positive Addition

Informal description

For any extended nonnegative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the strict inequality $a < b$ holds if and only if there exists a positive nonnegative real number $r > 0$ such that $a + r < b$.

ENNReal.le_of_forall_pos_le_add theorem

(h : ∀ ε : ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) : a ≤ b

Full source

theorem le_of_forall_pos_le_add (h : ∀ ε : ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) : a ≤ b := by
  contrapose! h
  rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩
  exact ⟨r, hr0, h.trans_le le_top, hr⟩

Limit Characterization of Inequality in Extended Nonnegative Reals

Informal description

For any extended nonnegative real numbers $a$ and $b$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, if for every positive $\varepsilon \in \mathbb{R}_{\geq 0}$ with $b < \infty$ we have $a \leq b + \varepsilon$, then $a \leq b$.

ENNReal.natCast_lt_coe theorem

{n : ℕ} : n < (r : ℝ≥0∞) ↔ n < r

Full source

theorem natCast_lt_coe {n : ℕ} : n < (r : ℝ≥0∞) ↔ n < r := ENNReal.coe_natCast n ▸ coe_lt_coe

Natural Number Comparison in Extended Nonnegative Reals: $n < r$

Informal description

For any natural number $n$ and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $n < r$ holds in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $n < r$ holds in $\mathbb{R}_{\geq 0}$ (when $r$ is finite).

ENNReal.coe_lt_natCast theorem

{n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n

Full source

theorem coe_lt_natCast {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n := ENNReal.coe_natCast n ▸ coe_lt_coe

Inequality Preservation: $\overline{r} < n \leftrightarrow r < n$ in Extended Nonnegative Reals

Informal description

For any nonnegative real number $r$ and any natural number $n$, the inequality $\overline{r} < n$ holds in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $r < n$ holds in $\mathbb{R}_{\geq 0}$, where $\overline{r}$ denotes the canonical inclusion of $r$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.exists_nat_gt theorem

{r : ℝ≥0∞} (h : r ≠ ∞) : ∃ n : ℕ, r < n

Full source

protected theorem exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃ n : ℕ, r < n := by
  lift r to ℝ≥0 using h
  rcases exists_nat_gt r with ⟨n, hn⟩
  exact ⟨n, coe_lt_natCast.2 hn⟩

Existence of Natural Number Exceeding Finite Extended Nonnegative Real Number

Informal description

For any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $r \neq \infty$, there exists a natural number $n$ such that $r < n$.

ENNReal.iUnion_Iio_coe_nat theorem

: ⋃ n : ℕ, Iio (n : ℝ≥0∞) = {∞}ᶜ

Full source

@[simp]
theorem iUnion_Iio_coe_nat : ⋃ n : ℕ, Iio (n : ℝ≥0∞) = {∞}{∞}ᶜ := by
  ext x
  rw [mem_iUnion]
  exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

Union of intervals $(-\infty, n)$ equals finite extended nonnegative reals

Informal description

The union over all natural numbers $n$ of the left-infinite right-open intervals $(-\infty, n)$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the complement of the singleton set $\{\infty\}$. In other words, $$\bigcup_{n \in \mathbb{N}} (-\infty, n) = \mathbb{R}_{\geq 0}.$$

ENNReal.iUnion_Iic_coe_nat theorem

: ⋃ n : ℕ, Iic (n : ℝ≥0∞) = {∞}ᶜ

Full source

@[simp]
theorem iUnion_Iic_coe_nat : ⋃ n : ℕ, Iic (n : ℝ≥0∞) = {∞}{∞}ᶜ :=
  Subset.antisymm (iUnion_subset fun n _x hx => ne_top_of_le_ne_top (natCast_ne_top n) hx) <|
    iUnion_Iio_coe_nat ▸ iUnion_mono fun _ => Iio_subset_Iic_self

Union of Closed Intervals $(-\infty, n]$ Equals Finite Extended Nonnegative Reals

Informal description

The union over all natural numbers $n$ of the left-infinite right-closed intervals $(-\infty, n]$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the complement of the singleton set $\{\infty\}$. In other words, $$\bigcup_{n \in \mathbb{N}} (-\infty, n] = \mathbb{R}_{\geq 0}.$$

ENNReal.iUnion_Ioc_coe_nat theorem

: ⋃ n : ℕ, Ioc a n = Ioi a \ {∞}

Full source

@[simp]
theorem iUnion_Ioc_coe_nat : ⋃ n : ℕ, Ioc a n = IoiIoi a \ {∞} := by
  simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Union of Half-Open Intervals $(a, n]$ Equals $(a, \infty) \setminus \{\infty\}$ in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a$, the union over all natural numbers $n$ of the left-open right-closed intervals $(a, n]$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the set of all numbers strictly greater than $a$ except for $\infty$. In other words, $$\bigcup_{n \in \mathbb{N}} (a, n] = (a, \infty) \setminus \{\infty\}.$$

ENNReal.iUnion_Ioo_coe_nat theorem

: ⋃ n : ℕ, Ioo a n = Ioi a \ {∞}

Full source

@[simp]
theorem iUnion_Ioo_coe_nat : ⋃ n : ℕ, Ioo a n = IoiIoi a \ {∞} := by
  simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Union of Open Intervals $(a, n)$ Equals $(a, \infty) \setminus \{\infty\}$ in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a$, the union over all natural numbers $n$ of the open intervals $(a, n)$ in the extended nonnegative real numbers equals the set of all numbers strictly greater than $a$ except for $\infty$. In other words, $$\bigcup_{n \in \mathbb{N}} (a, n) = (a, \infty) \setminus \{\infty\}.$$

ENNReal.iUnion_Icc_coe_nat theorem

: ⋃ n : ℕ, Icc a n = Ici a \ {∞}

Full source

@[simp]
theorem iUnion_Icc_coe_nat : ⋃ n : ℕ, Icc a n = IciIci a \ {∞} := by
  simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Union of Closed Intervals $[a, n]$ Equals $[a, \infty) \setminus \{\infty\}$ in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the union over all natural numbers $n$ of the closed intervals $[a, n]$ equals the left-closed right-infinite interval $[a, \infty)$ minus the singleton set $\{\infty\}$. In other words, $$\bigcup_{n \in \mathbb{N}} [a, n] = [a, \infty) \setminus \{\infty\}.$$

ENNReal.iUnion_Ico_coe_nat theorem

: ⋃ n : ℕ, Ico a n = Ici a \ {∞}

Full source

@[simp]
theorem iUnion_Ico_coe_nat : ⋃ n : ℕ, Ico a n = IciIci a \ {∞} := by
  simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Union of Intervals $[a, n)$ Equals $[a, \infty) \setminus \{\infty\}$ in Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the union over all natural numbers $n$ of the left-closed right-open intervals $[a, n)$ equals the left-closed right-infinite interval $[a, \infty)$ minus the singleton set $\{\infty\}$. In other words, $$\bigcup_{n \in \mathbb{N}} [a, n) = [a, \infty) \setminus \{\infty\}.$$

ENNReal.iInter_Ici_coe_nat theorem

: ⋂ n : ℕ, Ici (n : ℝ≥0∞) = {∞}

Full source

@[simp]
theorem iInter_Ici_coe_nat : ⋂ n : ℕ, Ici (n : ℝ≥0∞) = {∞} := by
  simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]

Intersection of Intervals $[n, \infty)$ in Extended Nonnegative Reals is $\{\infty\}$

Informal description

The intersection over all natural numbers $n$ of the left-closed right-infinite intervals $[n, \infty)$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the singleton set $\{\infty\}$. In other words, $$\bigcap_{n \in \mathbb{N}} [n, \infty) = \{\infty\}.$$

ENNReal.iInter_Ioi_coe_nat theorem

: ⋂ n : ℕ, Ioi (n : ℝ≥0∞) = {∞}

Full source

@[simp]
theorem iInter_Ioi_coe_nat : ⋂ n : ℕ, Ioi (n : ℝ≥0∞) = {∞} := by
  simp only [← compl_Iic, ← compl_iUnion, iUnion_Iic_coe_nat, compl_compl]

Intersection of Open Intervals $(n, \infty)$ in Extended Nonnegative Reals Equals $\{\infty\}$

Informal description

The intersection over all natural numbers $n$ of the left-open right-infinite intervals $(n, \infty)$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the singleton set $\{\infty\}$. In other words, $$\bigcap_{n \in \mathbb{N}} (n, \infty) = \{\infty\}.$$

ENNReal.coe_min theorem

(r p : ℝ≥0) : ((min r p : ℝ≥0) : ℝ≥0∞) = min (r : ℝ≥0∞) p

Full source

@[simp, norm_cast]
theorem coe_min (r p : ℝ≥0) : ((min r p : ℝ≥0) : ℝ≥0∞) = min (r : ℝ≥0∞) p := rfl

Minimum Operation Commutes with Inclusion into Extended Nonnegative Reals

Informal description

For any two nonnegative real numbers $r$ and $p$, the canonical inclusion of their minimum $\min(r, p)$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the minimum of their individual inclusions, i.e., $(\min(r, p) : \mathbb{R}_{\geq 0} \cup \{\infty\}) = \min((r : \mathbb{R}_{\geq 0} \cup \{\infty\}), (p : \mathbb{R}_{\geq 0} \cup \{\infty\}))$.

ENNReal.coe_max theorem

(r p : ℝ≥0) : ((max r p : ℝ≥0) : ℝ≥0∞) = max (r : ℝ≥0∞) p

Full source

@[simp, norm_cast]
theorem coe_max (r p : ℝ≥0) : ((max r p : ℝ≥0) : ℝ≥0∞) = max (r : ℝ≥0∞) p := rfl

Max Operation Commutes with Inclusion into Extended Nonnegative Reals

Informal description

For any two nonnegative real numbers $r$ and $p$, the canonical injection of their maximum $\max(r, p)$ into the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the maximum of their individual injections, i.e., $(\max(r, p) : \mathbb{R}_{\geq 0} \cup \{\infty\}) = \max((r : \mathbb{R}_{\geq 0} \cup \{\infty\}), (p : \mathbb{R}_{\geq 0} \cup \{\infty\}))$.

ENNReal.le_of_top_imp_top_of_toNNReal_le theorem

 {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤) (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b

Full source

theorem le_of_top_imp_top_of_toNNReal_le {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤)
    (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b := by
  by_contra! hlt
  lift b to ℝ≥0 using hlt.ne_top
  lift a to ℝ≥0 using mt h coe_ne_top
  refine hlt.not_le ?_
  simpa using h_nnreal

Comparison of Extended Nonnegative Reals via Top and Underlying Values

Informal description

For any extended nonnegative real numbers $a$ and $b$, if $a = \infty$ implies $b = \infty$, and whenever $a \neq \infty$ and $b \neq \infty$ we have $a.\text{toNNReal} \leq b.\text{toNNReal}$, then $a \leq b$.

ENNReal.abs_toReal theorem

{x : ℝ≥0∞} : |x.toReal| = x.toReal

Full source

@[simp]
theorem abs_toReal {x : ℝ≥0∞} : |x.toReal| = x.toReal := by cases x <;> simp

Absolute Value of Extended Nonnegative Real Conversion

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the absolute value of its real conversion equals its real conversion, i.e., $|x.\text{toReal}| = x.\text{toReal}$.

ENNReal.coe_sSup theorem

{s : Set ℝ≥0} : BddAbove s → (↑(sSup s) : ℝ≥0∞) = ⨆ a ∈ s, ↑a

Full source

theorem coe_sSup {s : Set ℝ≥0} : BddAbove s → (↑(sSup s) : ℝ≥0∞) = ⨆ a ∈ s, ↑a :=
  WithTop.coe_sSup

Supremum Commutes with Embedding of Bounded Nonnegative Real Sets into Extended Reals

Informal description

For any bounded above set $s$ of nonnegative real numbers, the image of its supremum under the canonical embedding into the extended nonnegative reals equals the supremum of the images of all elements in $s$. That is, $\overline{\sup s} = \bigsqcup_{a \in s} \overline{a}$, where $\overline{a}$ denotes the embedding of $a \in \mathbb{R}_{\geq 0}$ into $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

ENNReal.coe_sInf theorem

{s : Set ℝ≥0} (hs : s.Nonempty) : (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a

Full source

theorem coe_sInf {s : Set ℝ≥0} (hs : s.Nonempty) : (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a :=
  WithTop.coe_sInf hs (OrderBot.bddBelow s)

Infimum Preservation under Canonical Embedding to Extended Nonnegative Reals

Informal description

For any nonempty set $s$ of nonnegative real numbers, the canonical embedding of the infimum of $s$ into the extended nonnegative real numbers equals the infimum of the canonical embeddings of all elements in $s$. That is, $\uparrow(\inf s) = \inf_{a \in s} \uparrow a$.

ENNReal.coe_iSup theorem

{ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) : (↑(iSup f) : ℝ≥0∞) = ⨆ a, ↑(f a)

Full source

theorem coe_iSup {ι : Sort*} {f : ι → ℝ≥0} (hf : BddAbove (range f)) :
    (↑(iSup f) : ℝ≥0∞) = ⨆ a, ↑(f a) :=
  WithTop.coe_iSup _ hf

Canonical Embedding Preserves Supremum of Bounded Family in Extended Nonnegative Reals

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of nonnegative real numbers indexed by $\iota$, and suppose the range of $f$ is bounded above. Then the canonical embedding of the supremum of $f$ into the extended nonnegative real numbers equals the supremum of the canonical embeddings of the $f_i$: \[ \uparrow\left(\bigsqcup_{i} f_i\right) = \bigsqcup_{i} \uparrow f_i \]

ENNReal.coe_iInf theorem

{ι : Sort*} [Nonempty ι] (f : ι → ℝ≥0) : (↑(iInf f) : ℝ≥0∞) = ⨅ a, ↑(f a)

Full source

@[norm_cast]
theorem coe_iInf {ι : Sort*} [Nonempty ι] (f : ι → ℝ≥0) : (↑(iInf f) : ℝ≥0∞) = ⨅ a, ↑(f a) :=
  WithTop.coe_iInf (OrderBot.bddBelow _)

Infimum Preservation under Canonical Inclusion in Extended Nonnegative Reals

Informal description

For any nonempty index type $\iota$ and any function $f : \iota \to \mathbb{R}_{\geq 0}$, the canonical inclusion of the infimum of $f$ in $\mathbb{R}_{\geq 0}$ equals the infimum of the canonical inclusions of the values of $f$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$. That is, $\uparrow(\bigsqcap_{i} f(i)) = \bigsqcap_{i} \uparrow(f(i))$.

ENNReal.coe_mem_upperBounds theorem

{s : Set ℝ≥0} : ↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s

Full source

theorem coe_mem_upperBounds {s : Set ℝ≥0} :
    ↑r ∈ upperBounds (ofNNReal '' s)↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s := by
  simp +contextual [upperBounds, forall_mem_image, -mem_image, *]

Characterization of Upper Bounds under Canonical Injection in Extended Nonnegative Reals

Informal description

For any set $s$ of nonnegative real numbers and any $r \in \mathbb{R}_{\geq 0}$, the extended nonnegative real number $\uparrow r$ is an upper bound for the image of $s$ under the canonical injection $\text{ofNNReal} : \mathbb{R}_{\geq 0} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ if and only if $r$ is an upper bound for $s$ itself. In other words, $\uparrow r \in \text{upperBounds}(\text{ofNNReal} \ '' \ s) \leftrightarrow r \in \text{upperBounds}(s)$.

ENNReal.iSup_coe_eq_top theorem

: ⨆ i, (f i : ℝ≥0∞) = ⊤ ↔ ¬BddAbove (range f)

Full source

lemma iSup_coe_eq_top : ⨆ i, (f i : ℝ≥0∞)⨆ i, (f i : ℝ≥0∞) = ⊤ ↔ ¬ BddAbove (range f) := WithTop.iSup_coe_eq_top

Supremum Equals Infinity in Extended Nonnegative Reals if and only if Unbounded Above

Informal description

For any indexed family of nonnegative real numbers $(f_i)_{i \in \iota}$, the supremum of their images in the extended nonnegative real numbers equals $\infty$ if and only if the range of $f$ is not bounded above. In other words, $$ \bigsqcup_{i} (f_i : \mathbb{R}_{\geq 0} \cup \{\infty\}) = \infty \leftrightarrow \text{the set } \{f_i \mid i \in \iota\} \text{ has no upper bound in } \mathbb{R}_{\geq 0}. $$

ENNReal.iSup_coe_lt_top theorem

: ⨆ i, (f i : ℝ≥0∞) < ⊤ ↔ BddAbove (range f)

Full source

lemma iSup_coe_lt_top : ⨆ i, (f i : ℝ≥0∞)⨆ i, (f i : ℝ≥0∞) < ⊤ ↔ BddAbove (range f) := WithTop.iSup_coe_lt_top

Supremum of Extended Nonnegative Reals is Finite if and only if the Family is Bounded Above

Informal description

For any indexed family of nonnegative real numbers $(f_i)_{i \in \iota}$, the supremum of their images in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is strictly less than $\infty$ if and only if the range of $f$ is bounded above in $\mathbb{R}_{\geq 0}$. In other words, $\bigsqcup_{i} (f_i : \mathbb{R}_{\geq 0} \cup \{\infty\}) < \infty \leftrightarrow \text{the set } \{f_i \mid i \in \iota\} \text{ is bounded above in } \mathbb{R}_{\geq 0}$.

ENNReal.iInf_coe_eq_top theorem

: ⨅ i, (f i : ℝ≥0∞) = ⊤ ↔ IsEmpty ι

Full source

lemma iInf_coe_eq_top : ⨅ i, (f i : ℝ≥0∞)⨅ i, (f i : ℝ≥0∞) = ⊤ ↔ IsEmpty ι := WithTop.iInf_coe_eq_top

Infimum of Extended Nonnegative Reals is Infinity if and only if Index Set is Empty

Informal description

For any indexed family of extended nonnegative real numbers $(f_i : \mathbb{R}_{\geq 0} \cup \{\infty\})_{i \in \iota}$, the infimum $\bigsqcap_{i} f_i$ equals $\infty$ if and only if the index set $\iota$ is empty.

ENNReal.iInf_coe_lt_top theorem

: ⨅ i, (f i : ℝ≥0∞) < ⊤ ↔ Nonempty ι

Full source

lemma iInf_coe_lt_top : ⨅ i, (f i : ℝ≥0∞)⨅ i, (f i : ℝ≥0∞) < ⊤ ↔ Nonempty ι := WithTop.iInf_coe_lt_top

Infimum of Extended Nonnegative Reals is Less Than Infinity if and Only if Index Set is Nonempty

Informal description

For any indexed family of extended nonnegative real numbers $(f_i : \mathbb{R}_{\geq 0} \cup \{\infty\})$, the infimum $\bigsqcap_i f_i$ is strictly less than $\infty$ if and only if the index set is nonempty. In other words, $\bigsqcap_i f_i < \infty \leftrightarrow \text{Nonempty} \iota$.

Set.OrdConnected.preimage_coe_nnreal_ennreal theorem

(h : u.OrdConnected) : ((↑) ⁻¹' u : Set ℝ≥0).OrdConnected

Full source

theorem preimage_coe_nnreal_ennreal (h : u.OrdConnected) : ((↑)(↑) ⁻¹' u : Set ℝ≥0).OrdConnected :=
  h.preimage_mono ENNReal.coe_mono

Preimage of Order-Connected Set under Inclusion from Nonnegative to Extended Nonnegative Reals is Order-Connected

Informal description

Let $u$ be an order-connected subset of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$. Then the preimage of $u$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is an order-connected subset of $\mathbb{R}_{\geq 0}$.

Set.OrdConnected.image_coe_nnreal_ennreal theorem

(h : t.OrdConnected) : ((↑) '' t : Set ℝ≥0∞).OrdConnected

Full source

theorem image_coe_nnreal_ennreal (h : t.OrdConnected) : ((↑)(↑) '' t : Set ℝ≥0∞).OrdConnected := by
  refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
  rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩
  exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

Order-connectedness is preserved under inclusion into extended nonnegative reals

Informal description

Let $t$ be an order-connected subset of the nonnegative real numbers $\mathbb{R}_{\geq 0}$. Then the image of $t$ under the canonical inclusion map $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is also order-connected in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

Set.OrdConnected.preimage_ennreal_ofReal theorem

(h : u.OrdConnected) : (ENNReal.ofReal ⁻¹' u).OrdConnected

Full source

theorem preimage_ennreal_ofReal (h : u.OrdConnected) : (ENNReal.ofRealENNReal.ofReal ⁻¹' u).OrdConnected :=
  h.preimage_coe_nnreal_ennreal.preimage_real_toNNReal

Preimage of Order-Connected Set under $\text{ENNReal.ofReal}$ is Order-Connected

Informal description

Let $u$ be an order-connected subset of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$. Then the preimage of $u$ under the function $\text{ENNReal.ofReal} : \mathbb{R} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, which maps $x$ to $\max(x, 0)$, is an order-connected subset of $\mathbb{R}$.

Set.OrdConnected.image_ennreal_ofReal theorem

(h : s.OrdConnected) : (ENNReal.ofReal '' s).OrdConnected

Full source

theorem image_ennreal_ofReal (h : s.OrdConnected) : (ENNReal.ofRealENNReal.ofReal '' s).OrdConnected := by
  simpa only [image_image] using h.image_real_toNNReal.image_coe_nnreal_ennreal

Order-connectedness is preserved under $\text{ENNReal.ofReal}$ mapping

Informal description

Let $s$ be an order-connected subset of the real numbers. Then the image of $s$ under the function $\text{ENNReal.ofReal} : \mathbb{R} \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, which maps $x$ to $\max(x, 0)$, is also order-connected in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

instReprENNReal instance

: Repr ℝ≥0∞

Full source

/-- While not very useful, this instance uses the same representation as `Real.instRepr`. -/
unsafe instance : Repr ℝ≥0∞ where
  reprPrec
  | (r : ℝ≥0), p => Repr.addAppParen f!"ENNReal.ofReal ({repr r.val})" p
  | ∞, _ => "∞"

String Representation of Extended Nonnegative Real Numbers

Informal description

The extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ have a representation as strings, similar to the representation of real numbers.

Mathlib.Meta.Positivity.evalENNRealtoReal definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: `ENNReal.toReal`. -/
@[positivity ENNReal.toReal _]
def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(ENNReal.toReal $a) =>
    assertInstancesCommute
    pure (.nonnegative q(ENNReal.toReal_nonneg))
  | _, _, _ => throwError "not ENNReal.toReal"

Nonnegativity of extended nonnegative reals under real conversion

Informal description

The positivity extension for the function `ENNReal.toReal` states that for any extended nonnegative real number `a`, its conversion to a real number via `ENNReal.toReal` yields a nonnegative value. That is, `ENNReal.toReal a ≥ 0` for all `a ∈ ℝ≥0∞`.

Mathlib.Meta.Positivity.evalENNRealOfNNReal definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: `ENNReal.ofNNReal`. -/
@[positivity ENNReal.ofNNReal _]
def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofNNReal $a) =>
    let ra ← core q(inferInstance) q(inferInstance) a
    assertInstancesCommute
    match ra with
    | .positive pa => pure <| .positive q(ENNReal.coe_pos.mpr $pa)
    | _ => pure .none
  | _, _, _ => throwError "not ENNReal.ofNNReal"

Extension of nonnegative real numbers to extended nonnegative reals

Informal description

The function `ENNReal.ofNNReal` maps a nonnegative real number `a` to its corresponding extended nonnegative real number in `ℝ≥0∞`. This is part of the positivity tactic extension for handling extended nonnegative real numbers.

Mathlib.Data.ENNReal.Basic

Main definitions

Implementation notes

Notations