Documentation

Mathlib.Data.NNReal.Defs

Nonnegative real numbers #

In this file we define NNReal (notation: ℝ≥0) to be the type of non-negative real numbers, a.k.a. the interval [0, ∞). We also define the following operations and structures on ℝ≥0:

We also define an instance CanLift ℝ ℝ≥0. This instance can be used by the lift tactic to replace x : ℝ and hx : 0 ≤ x in the proof context with x : ℝ≥0 while replacing all occurrences of x with ↑x. This tactic also works for a function f : α → ℝ with a hypothesis hf : ∀ x, 0 ≤ f x.

Notations #

This file defines ℝ≥0 as a localized notation for NNReal.

Nonnegative real numbers.

Equations
Instances For
    noncomputable instance NNReal.instSub :
    Equations

    Coercion ℝ≥0 → ℝ.

    Equations
    Instances For
      @[simp]
      theorem NNReal.val_eq_coe (n : NNReal) :
      n = n
      instance NNReal.canLift :
      Equations
      theorem NNReal.eq_iff {n : NNReal} {m : NNReal} :
      n = m n = m
      theorem NNReal.eq {n : NNReal} {m : NNReal} :
      n = mn = m
      theorem NNReal.ne_iff {x : NNReal} {y : NNReal} :
      x y x y
      theorem NNReal.forall {p : NNRealProp} :
      (∀ (x : NNReal), p x) ∀ (x : ) (hx : 0 x), p x, hx
      theorem NNReal.exists {p : NNRealProp} :
      (∃ (x : NNReal), p x) ∃ (x : ) (hx : 0 x), p x, hx
      noncomputable def Real.toNNReal (r : ) :

      Reinterpret a real number r as a non-negative real number. Returns 0 if r < 0.

      Equations
      • r.toNNReal = max r 0,
      Instances For
        theorem Real.coe_toNNReal (r : ) (hr : 0 r) :
        r.toNNReal = r
        theorem Real.toNNReal_of_nonneg {r : } (hr : 0 r) :
        r.toNNReal = r, hr
        theorem Real.le_coe_toNNReal (r : ) :
        r r.toNNReal
        theorem NNReal.coe_nonneg (r : NNReal) :
        0 r
        @[simp]
        theorem NNReal.coe_mk (a : ) (ha : 0 a) :
        a, ha = a
        @[simp]
        theorem NNReal.coe_inj {r₁ : NNReal} {r₂ : NNReal} :
        r₁ = r₂ r₁ = r₂
        @[deprecated NNReal.coe_inj]
        theorem NNReal.coe_eq {r₁ : NNReal} {r₂ : NNReal} :
        r₁ = r₂ r₁ = r₂

        Alias of NNReal.coe_inj.

        @[simp]
        theorem NNReal.coe_zero :
        0 = 0
        @[simp]
        theorem NNReal.coe_one :
        1 = 1
        @[simp]
        theorem NNReal.mk_zero :
        0, = 0
        @[simp]
        theorem NNReal.mk_one :
        1, = 1
        @[simp]
        theorem NNReal.coe_add (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ + r₂) = r₁ + r₂
        @[simp]
        theorem NNReal.coe_mul (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ * r₂) = r₁ * r₂
        @[simp]
        theorem NNReal.coe_inv (r : NNReal) :
        r⁻¹ = (↑r)⁻¹
        @[simp]
        theorem NNReal.coe_div (r₁ : NNReal) (r₂ : NNReal) :
        (r₁ / r₂) = r₁ / r₂
        theorem NNReal.coe_two :
        2 = 2
        @[simp]
        theorem NNReal.coe_sub {r₁ : NNReal} {r₂ : NNReal} (h : r₂ r₁) :
        (r₁ - r₂) = r₁ - r₂
        @[simp]
        theorem NNReal.coe_eq_zero {r : NNReal} :
        r = 0 r = 0
        @[simp]
        theorem NNReal.coe_eq_one {r : NNReal} :
        r = 1 r = 1
        theorem NNReal.coe_ne_zero {r : NNReal} :
        r 0 r 0
        theorem NNReal.coe_ne_one {r : NNReal} :
        r 1 r 1

        Coercion ℝ≥0 → ℝ as a RingHom.

        Porting note (#11215): TODO: what if we define Coe ℝ≥0 ℝ using this function?

        Equations
        Instances For

          A MulAction over restricts to a MulAction over ℝ≥0.

          Equations
          theorem NNReal.smul_def {M : Type u_1} [MulAction M] (c : NNReal) (x : M) :
          c x = c x
          Equations
          • =
          instance NNReal.smulCommClass_left {M : Type u_1} {N : Type u_2} [MulAction N] [SMul M N] [SMulCommClass M N] :
          Equations
          • =
          instance NNReal.smulCommClass_right {M : Type u_1} {N : Type u_2} [MulAction N] [SMul M N] [SMulCommClass M N] :
          Equations
          • =

          A DistribMulAction over restricts to a DistribMulAction over ℝ≥0.

          Equations

          A Module over restricts to a Module over ℝ≥0.

          Equations

          An Algebra over restricts to an Algebra over ℝ≥0.

          Equations
          @[simp]
          theorem NNReal.coe_pow (r : NNReal) (n : ) :
          (r ^ n) = r ^ n
          @[simp]
          theorem NNReal.coe_zpow (r : NNReal) (n : ) :
          (r ^ n) = r ^ n
          @[simp]
          theorem NNReal.coe_nsmul (r : NNReal) (n : ) :
          (n r) = n r
          @[simp]
          theorem NNReal.coe_nnqsmul (q : ℚ≥0) (x : NNReal) :
          (q x) = q x
          @[simp]
          theorem NNReal.coe_natCast (n : ) :
          n = n
          @[deprecated NNReal.coe_natCast]
          theorem NNReal.coe_nat_cast (n : ) :
          n = n

          Alias of NNReal.coe_natCast.

          @[simp]
          theorem NNReal.coe_ofNat (n : ) [n.AtLeastTwo] :
          @[simp]
          theorem NNReal.coe_le_coe {r₁ : NNReal} {r₂ : NNReal} :
          r₁ r₂ r₁ r₂
          @[simp]
          theorem NNReal.coe_lt_coe {r₁ : NNReal} {r₂ : NNReal} :
          r₁ < r₂ r₁ < r₂
          @[simp]
          theorem NNReal.coe_pos {r : NNReal} :
          0 < r 0 < r
          @[simp]
          theorem NNReal.one_le_coe {r : NNReal} :
          1 r 1 r
          @[simp]
          theorem NNReal.one_lt_coe {r : NNReal} :
          1 < r 1 < r
          @[simp]
          theorem NNReal.coe_le_one {r : NNReal} :
          r 1 r 1
          @[simp]
          theorem NNReal.coe_lt_one {r : NNReal} :
          r < 1 r < 1
          theorem NNReal.GCongr.toReal_le_toReal {r₁ : NNReal} {r₂ : NNReal} :
          r₁ r₂r₁ r₂

          Alias for the use of gcongr

          @[simp]
          theorem Real.toNNReal_coe {r : NNReal} :
          (↑r).toNNReal = r
          @[simp]
          theorem NNReal.mk_natCast (n : ) :
          n, = n
          @[deprecated NNReal.mk_natCast]
          theorem NNReal.mk_coe_nat (n : ) :
          n, = n

          Alias of NNReal.mk_natCast.

          @[simp]
          theorem NNReal.toNNReal_coe_nat (n : ) :
          (↑n).toNNReal = n
          @[simp]
          theorem Real.toNNReal_ofNat (n : ) [n.AtLeastTwo] :
          (OfNat.ofNat n).toNNReal = OfNat.ofNat n
          def NNReal.orderIsoIccZeroCoe (a : NNReal) :
          (Set.Icc 0 a) ≃o (Set.Iic a)

          If a is a nonnegative real number, then the closed interval [0, a] in is order isomorphic to the interval Set.Iic a.

          Equations
          Instances For
            @[simp]
            theorem NNReal.orderIsoIccZeroCoe_apply_coe_coe (a : NNReal) (b : (Set.Icc 0 a)) :
            (a.orderIsoIccZeroCoe b) = b
            @[simp]
            theorem NNReal.orderIsoIccZeroCoe_symm_apply_coe (a : NNReal) (b : (Set.Iic a)) :
            (a.orderIsoIccZeroCoe.symm b) = b
            theorem NNReal.coe_image {s : Set NNReal} :
            NNReal.toReal '' s = {x : | ∃ (h : 0 x), x, h s}
            @[simp]
            theorem NNReal.coe_iSup {ι : Sort u_2} (s : ιNNReal) :
            (⨆ (i : ι), s i) = ⨆ (i : ι), (s i)
            @[simp]
            theorem NNReal.coe_iInf {ι : Sort u_2} (s : ιNNReal) :
            (⨅ (i : ι), s i) = ⨅ (i : ι), (s i)
            @[deprecated le_of_forall_pos_le_add]
            theorem NNReal.le_of_forall_pos_le_add {a : NNReal} {b : NNReal} (h : ∀ (ε : NNReal), 0 < εa b + ε) :
            a b
            theorem NNReal.lt_iff_exists_rat_btwn (a : NNReal) (b : NNReal) :
            a < b ∃ (q : ), 0 q a < (↑q).toNNReal (↑q).toNNReal < b
            theorem NNReal.mul_sup (a : NNReal) (b : NNReal) (c : NNReal) :
            a * (b c) = a * b a * c
            theorem NNReal.sup_mul (a : NNReal) (b : NNReal) (c : NNReal) :
            (a b) * c = a * c b * c
            @[simp]
            theorem NNReal.coe_max (x : NNReal) (y : NNReal) :
            (max x y) = max x y
            @[simp]
            theorem NNReal.coe_min (x : NNReal) (y : NNReal) :
            (min x y) = min x y
            @[simp]
            theorem NNReal.zero_le_coe {q : NNReal} :
            0 q
            @[simp]
            theorem Real.coe_toNNReal' (r : ) :
            r.toNNReal = max r 0
            @[simp]
            theorem Real.toNNReal_pos {r : } :
            0 < r.toNNReal 0 < r
            @[simp]
            theorem Real.toNNReal_eq_zero {r : } :
            r.toNNReal = 0 r 0
            theorem Real.toNNReal_of_nonpos {r : } :
            r 0r.toNNReal = 0
            theorem Real.toNNReal_eq_iff_eq_coe {r : } {p : NNReal} (hp : p 0) :
            r.toNNReal = p r = p
            @[simp]
            theorem Real.toNNReal_eq_one {r : } :
            r.toNNReal = 1 r = 1
            @[simp]
            theorem Real.toNNReal_eq_natCast {r : } {n : } (hn : n 0) :
            r.toNNReal = n r = n
            @[deprecated Real.toNNReal_eq_natCast]
            theorem Real.toNNReal_eq_nat_cast {r : } {n : } (hn : n 0) :
            r.toNNReal = n r = n

            Alias of Real.toNNReal_eq_natCast.

            @[simp]
            theorem Real.toNNReal_eq_ofNat {r : } {n : } [n.AtLeastTwo] :
            r.toNNReal = OfNat.ofNat n r = OfNat.ofNat n
            @[simp]
            theorem Real.toNNReal_le_toNNReal_iff {r : } {p : } (hp : 0 p) :
            r.toNNReal p.toNNReal r p
            @[simp]
            theorem Real.toNNReal_le_one {r : } :
            r.toNNReal 1 r 1
            @[simp]
            theorem Real.one_lt_toNNReal {r : } :
            1 < r.toNNReal 1 < r
            @[simp]
            theorem Real.toNNReal_le_natCast {r : } {n : } :
            r.toNNReal n r n
            @[deprecated Real.toNNReal_le_natCast]
            theorem Real.toNNReal_le_nat_cast {r : } {n : } :
            r.toNNReal n r n

            Alias of Real.toNNReal_le_natCast.

            @[simp]
            theorem Real.natCast_lt_toNNReal {r : } {n : } :
            n < r.toNNReal n < r
            @[deprecated Real.natCast_lt_toNNReal]
            theorem Real.nat_cast_lt_toNNReal {r : } {n : } :
            n < r.toNNReal n < r

            Alias of Real.natCast_lt_toNNReal.

            @[simp]
            theorem Real.toNNReal_le_ofNat {r : } {n : } [n.AtLeastTwo] :
            r.toNNReal OfNat.ofNat n r n
            @[simp]
            theorem Real.ofNat_lt_toNNReal {r : } {n : } [n.AtLeastTwo] :
            OfNat.ofNat n < r.toNNReal n < r
            @[simp]
            theorem Real.toNNReal_eq_toNNReal_iff {r : } {p : } (hr : 0 r) (hp : 0 p) :
            r.toNNReal = p.toNNReal r = p
            @[simp]
            theorem Real.toNNReal_lt_toNNReal_iff' {r : } {p : } :
            r.toNNReal < p.toNNReal r < p 0 < p
            theorem Real.toNNReal_lt_toNNReal_iff {r : } {p : } (h : 0 < p) :
            r.toNNReal < p.toNNReal r < p
            theorem Real.lt_of_toNNReal_lt {r : } {p : } (h : r.toNNReal < p.toNNReal) :
            r < p
            theorem Real.toNNReal_lt_toNNReal_iff_of_nonneg {r : } {p : } (hr : 0 r) :
            r.toNNReal < p.toNNReal r < p
            theorem Real.toNNReal_le_toNNReal_iff' {r : } {p : } :
            r.toNNReal p.toNNReal r p r 0
            theorem Real.toNNReal_le_toNNReal_iff_of_pos {r : } {p : } (hr : 0 < r) :
            r.toNNReal p.toNNReal r p
            @[simp]
            theorem Real.one_le_toNNReal {r : } :
            1 r.toNNReal 1 r
            @[simp]
            theorem Real.toNNReal_lt_one {r : } :
            r.toNNReal < 1 r < 1
            @[simp]
            theorem Real.natCastle_toNNReal' {n : } {r : } :
            n r.toNNReal n r n = 0
            @[deprecated Real.natCastle_toNNReal']
            theorem Real.nat_cast_le_toNNReal' {n : } {r : } :
            n r.toNNReal n r n = 0

            Alias of Real.natCastle_toNNReal'.

            @[simp]
            theorem Real.toNNReal_lt_natCast' {n : } {r : } :
            r.toNNReal < n r < n n 0
            @[deprecated Real.toNNReal_lt_natCast']
            theorem Real.toNNReal_lt_nat_cast' {n : } {r : } :
            r.toNNReal < n r < n n 0

            Alias of Real.toNNReal_lt_natCast'.

            theorem Real.natCast_le_toNNReal {n : } {r : } (hn : n 0) :
            n r.toNNReal n r
            @[deprecated Real.natCast_le_toNNReal]
            theorem Real.nat_cast_le_toNNReal {n : } {r : } (hn : n 0) :
            n r.toNNReal n r

            Alias of Real.natCast_le_toNNReal.

            theorem Real.toNNReal_lt_natCast {r : } {n : } (hn : n 0) :
            r.toNNReal < n r < n
            @[deprecated Real.toNNReal_lt_natCast]
            theorem Real.toNNReal_lt_nat_cast {r : } {n : } (hn : n 0) :
            r.toNNReal < n r < n

            Alias of Real.toNNReal_lt_natCast.

            @[simp]
            theorem Real.toNNReal_lt_ofNat {r : } {n : } [n.AtLeastTwo] :
            r.toNNReal < OfNat.ofNat n r < OfNat.ofNat n
            @[simp]
            theorem Real.ofNat_le_toNNReal {n : } {r : } [n.AtLeastTwo] :
            OfNat.ofNat n r.toNNReal OfNat.ofNat n r
            @[simp]
            theorem Real.toNNReal_add {r : } {p : } (hr : 0 r) (hp : 0 p) :
            (r + p).toNNReal = r.toNNReal + p.toNNReal
            theorem Real.toNNReal_add_toNNReal {r : } {p : } (hr : 0 r) (hp : 0 p) :
            r.toNNReal + p.toNNReal = (r + p).toNNReal
            theorem Real.toNNReal_le_toNNReal {r : } {p : } (h : r p) :
            r.toNNReal p.toNNReal
            theorem Real.toNNReal_add_le {r : } {p : } :
            (r + p).toNNReal r.toNNReal + p.toNNReal
            theorem Real.toNNReal_le_iff_le_coe {r : } {p : NNReal} :
            r.toNNReal p r p
            theorem Real.le_toNNReal_iff_coe_le {r : NNReal} {p : } (hp : 0 p) :
            r p.toNNReal r p
            theorem Real.le_toNNReal_iff_coe_le' {r : NNReal} {p : } (hr : 0 < r) :
            r p.toNNReal r p
            theorem Real.toNNReal_lt_iff_lt_coe {r : } {p : NNReal} (ha : 0 r) :
            r.toNNReal < p r < p
            theorem Real.lt_toNNReal_iff_coe_lt {r : NNReal} {p : } :
            r < p.toNNReal r < p
            theorem Real.toNNReal_pow {x : } (hx : 0 x) (n : ) :
            (x ^ n).toNNReal = x.toNNReal ^ n
            theorem Real.toNNReal_mul {p : } {q : } (hp : 0 p) :
            (p * q).toNNReal = p.toNNReal * q.toNNReal
            theorem NNReal.mul_eq_mul_left {a : NNReal} {b : NNReal} {c : NNReal} (h : a 0) :
            a * b = a * c b = c
            theorem NNReal.pow_antitone_exp {a : NNReal} (m : ) (n : ) (mn : m n) (a1 : a 1) :
            a ^ n a ^ m
            theorem NNReal.exists_pow_lt_of_lt_one {a : NNReal} {b : NNReal} (ha : 0 < a) (hb : b < 1) :
            ∃ (n : ), b ^ n < a
            theorem NNReal.exists_mem_Ico_zpow {x : NNReal} {y : NNReal} (hx : x 0) (hy : 1 < y) :
            ∃ (n : ), x Set.Ico (y ^ n) (y ^ (n + 1))
            theorem NNReal.exists_mem_Ioc_zpow {x : NNReal} {y : NNReal} (hx : x 0) (hy : 1 < y) :
            ∃ (n : ), x Set.Ioc (y ^ n) (y ^ (n + 1))

            Lemmas about subtraction #

            In this section we provide a few lemmas about subtraction that do not fit well into any other typeclass. For lemmas about subtraction and addition see lemmas about OrderedSub in the file Mathlib.Algebra.Order.Sub.Basic. See also mul_tsub and tsub_mul.

            theorem NNReal.sub_def {r : NNReal} {p : NNReal} :
            r - p = (r - p).toNNReal
            theorem NNReal.coe_sub_def {r : NNReal} {p : NNReal} :
            (r - p) = max (r - p) 0
            @[simp]
            theorem NNReal.inv_le {r : NNReal} {p : NNReal} (h : r 0) :
            r⁻¹ p 1 r * p
            theorem NNReal.inv_le_of_le_mul {r : NNReal} {p : NNReal} (h : 1 r * p) :
            @[simp]
            theorem NNReal.le_inv_iff_mul_le {r : NNReal} {p : NNReal} (h : p 0) :
            r p⁻¹ r * p 1
            @[simp]
            theorem NNReal.lt_inv_iff_mul_lt {r : NNReal} {p : NNReal} (h : p 0) :
            r < p⁻¹ r * p < 1
            @[deprecated le_inv_mul_iff₀]
            theorem NNReal.mul_le_iff_le_inv {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            r * a b a r⁻¹ * b
            @[deprecated le_div_iff₀]
            theorem NNReal.le_div_iff_mul_le {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r a * r b
            @[deprecated div_le_iff₀]
            theorem NNReal.div_le_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r b a b * r
            @[deprecated div_le_iff₀']
            theorem NNReal.div_le_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r b a r * b
            theorem NNReal.div_le_of_le_mul {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
            a / c b
            theorem NNReal.div_le_of_le_mul' {a : NNReal} {b : NNReal} {c : NNReal} (h : a b * c) :
            a / b c
            @[deprecated le_div_iff₀]
            theorem NNReal.le_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r a * r b
            @[deprecated le_div_iff₀']
            theorem NNReal.le_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a b / r r * a b
            @[deprecated div_lt_iff₀]
            theorem NNReal.div_lt_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r < b a < b * r
            @[deprecated div_lt_iff₀']
            theorem NNReal.div_lt_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a / r < b a < r * b
            @[deprecated lt_div_iff₀]
            theorem NNReal.lt_div_iff {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a < b / r a * r < b
            @[deprecated lt_div_iff₀']
            theorem NNReal.lt_div_iff' {a : NNReal} {b : NNReal} {r : NNReal} (hr : r 0) :
            a < b / r r * a < b
            theorem NNReal.mul_lt_of_lt_div {a : NNReal} {b : NNReal} {r : NNReal} (h : a < b / r) :
            a * r < b
            theorem NNReal.div_le_div_left_of_le {a : NNReal} {b : NNReal} {c : NNReal} (c0 : c 0) (cb : c b) :
            a / b a / c
            theorem NNReal.div_le_div_left {a : NNReal} {b : NNReal} {c : NNReal} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
            a / b a / c c b
            theorem NNReal.le_of_forall_lt_one_mul_le {x : NNReal} {y : NNReal} (h : a < 1, a * x y) :
            x y
            theorem NNReal.half_le_self (a : NNReal) :
            a / 2 a
            theorem NNReal.half_lt_self {a : NNReal} (h : a 0) :
            a / 2 < a
            theorem NNReal.div_lt_one_of_lt {a : NNReal} {b : NNReal} (h : a < b) :
            a / b < 1
            theorem Real.toNNReal_inv {x : } :
            x⁻¹.toNNReal = x.toNNReal⁻¹
            theorem Real.toNNReal_div {x : } {y : } (hx : 0 x) :
            (x / y).toNNReal = x.toNNReal / y.toNNReal
            theorem Real.toNNReal_div' {x : } {y : } (hy : 0 y) :
            (x / y).toNNReal = x.toNNReal / y.toNNReal
            theorem NNReal.inv_lt_one_iff {x : NNReal} (hx : x 0) :
            x⁻¹ < 1 1 < x
            @[deprecated zpow_pos]
            theorem NNReal.zpow_pos {x : NNReal} (hx : x 0) (n : ) :
            0 < x ^ n
            theorem NNReal.inv_lt_inv {x : NNReal} {y : NNReal} (hx : x 0) (h : x < y) :
            @[simp]
            theorem NNReal.abs_eq (x : NNReal) :
            |x| = x
            theorem NNReal.le_toNNReal_of_coe_le {x : NNReal} {y : } (h : x y) :
            x y.toNNReal
            theorem NNReal.iSup_of_not_bddAbove {ι : Sort u_1} {f : ιNNReal} (hf : ¬BddAbove (Set.range f)) :
            ⨆ (i : ι), f i = 0
            theorem NNReal.iSup_empty {ι : Sort u_1} [IsEmpty ι] (f : ιNNReal) :
            ⨆ (i : ι), f i = 0
            theorem NNReal.iInf_empty {ι : Sort u_1} [IsEmpty ι] (f : ιNNReal) :
            ⨅ (i : ι), f i = 0
            @[simp]
            theorem NNReal.iSup_eq_zero {ι : Sort u_1} {f : ιNNReal} (hf : BddAbove (Set.range f)) :
            ⨆ (i : ι), f i = 0 ∀ (i : ι), f i = 0
            @[simp]
            theorem NNReal.iInf_const_zero {α : Sort u_2} :
            ⨅ (x : α), 0 = 0
            theorem Set.OrdConnected.preimage_coe_nnreal_real {s : Set } (h : s.OrdConnected) :
            (NNReal.toReal ⁻¹' s).OrdConnected
            theorem Set.OrdConnected.image_coe_nnreal_real {t : Set NNReal} (h : t.OrdConnected) :
            (NNReal.toReal '' t).OrdConnected
            theorem Set.OrdConnected.image_real_toNNReal {s : Set } (h : s.OrdConnected) :
            (Real.toNNReal '' s).OrdConnected
            theorem Set.OrdConnected.preimage_real_toNNReal {t : Set NNReal} (h : t.OrdConnected) :
            (Real.toNNReal ⁻¹' t).OrdConnected

            The absolute value on as a map to ℝ≥0.

            Equations
            Instances For
              @[simp]
              theorem Real.coe_nnabs (x : ) :
              (Real.nnabs x) = |x|
              @[simp]
              theorem Real.nnabs_of_nonneg {x : } (h : 0 x) :
              Real.nnabs x = x.toNNReal
              theorem Real.nnabs_coe (x : NNReal) :
              Real.nnabs x = x
              theorem Real.coe_toNNReal_le (x : ) :
              x.toNNReal |x|
              @[simp]
              theorem Real.toNNReal_abs (x : ) :
              |x|.toNNReal = Real.nnabs x
              theorem Real.cast_natAbs_eq_nnabs_cast (n : ) :
              n.natAbs = Real.nnabs n
              theorem NNReal.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono f) {r : NNReal} (hr : 0 < r) :
              ∃ (d : Γ₀ˣ), f d < r

              If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive r : ℝ≥0, there exists d : Γ₀ˣ with f d < r.

              theorem Real.exists_lt_of_strictMono {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ NNReal} (hf : StrictMono f) {r : } (hr : 0 < r) :
              ∃ (d : Γ₀ˣ), (f d) < r

              If Γ₀ˣ is nontrivial and f : Γ₀ →*₀ ℝ≥0 is strictly monotone, then for any positive real r, there exists d : Γ₀ˣ with f d < r.

              Extension for the positivity tactic: cast from ℝ≥0 to .

              Instances For