Documentation

Mathlib.Data.ENat.Basic

Definition and basic properties of extended natural numbers #

In this file we define ENat (notation: ℕ∞) to be WithTop and prove some basic lemmas about this type.

Implementation details #

There are two natural coercions from to WithTop ℕ = ENat: WithTop.some and Nat.cast. In Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally equal, we did not duplicate generic lemmas about WithTop α and WithTop.some coercion for ENat and Nat.cast coercion. If you need to apply a lemma about WithTop, you may either rewrite back and forth using ENat.some_eq_coe, or restate the lemma for ENat.

TODO #

Unify ENat.add_iSup/ENat.iSup_add with ENNReal.add_iSup/ENNReal.iSup_add. The key property of ENat and ENNReal we are using is that all a are either absorbing for addition (a + b = a for all b), or that it's order-cancellable (a + b ≤ a + c → b ≤ c for all b, c), and similarly for multiplication.

Equations
    Equations
      Equations
        @[simp]

        Lemmas about WithTop expect (and can output) WithTop.some but the normal form for coercion ℕ → ℕ∞ is Nat.cast.

        theorem ENat.coe_inj {a b : } :
        a = b a = b
        theorem ENat.coe_zero :
        0 = 0
        theorem ENat.coe_one :
        1 = 1
        theorem ENat.coe_add (m n : ) :
        ↑(m + n) = m + n
        @[simp]
        theorem ENat.coe_sub (m n : ) :
        ↑(m - n) = m - n
        @[simp]
        theorem ENat.coe_mul (m n : ) :
        ↑(m * n) = m * n
        @[simp]
        theorem ENat.mul_top {m : ℕ∞} (hm : m 0) :
        @[simp]
        theorem ENat.top_mul {m : ℕ∞} (hm : m 0) :
        theorem ENat.mul_top' {m : ℕ∞} :
        m * = if m = 0 then 0 else

        A version of mul_top where the RHS is stated as an ite

        theorem ENat.top_mul' {m : ℕ∞} :
        * m = if m = 0 then 0 else

        A version of top_mul where the RHS is stated as an ite

        @[simp]
        theorem ENat.top_pow {n : } (hn : n 0) :
        @[simp]
        theorem ENat.pow_eq_top_iff {a : ℕ∞} {n : } :
        a ^ n = a = n 0
        theorem ENat.pow_ne_top_iff {a : ℕ∞} {n : } :
        a ^ n a n = 0
        @[simp]
        theorem ENat.pow_lt_top_iff {a : ℕ∞} {n : } :
        a ^ n < a < n = 0
        theorem ENat.eq_top_of_pow {a : ℕ∞} (n : ) (ha : a ^ n = ) :
        a =
        def ENat.lift (x : ℕ∞) (h : x < ) :

        Convert a ℕ∞ to a using a proof that it is not infinite.

        Equations
          Instances For
            @[simp]
            theorem ENat.coe_lift (x : ℕ∞) (h : x < ) :
            (x.lift h) = x
            @[simp]
            theorem ENat.lift_coe (n : ) :
            (↑n).lift = n
            @[simp]
            theorem ENat.lift_lt_iff {x : ℕ∞} {h : x < } {n : } :
            x.lift h < n x < n
            @[simp]
            theorem ENat.lift_le_iff {x : ℕ∞} {h : x < } {n : } :
            x.lift h n x n
            @[simp]
            theorem ENat.lt_lift_iff {x : } {n : ℕ∞} {h : n < } :
            x < n.lift h x < n
            @[simp]
            theorem ENat.le_lift_iff {x : } {n : ℕ∞} {h : n < } :
            x n.lift h x n
            @[simp]
            theorem ENat.lift_zero :
            lift 0 = 0
            @[simp]
            theorem ENat.lift_one :
            lift 1 = 1
            @[simp]
            @[simp]
            theorem ENat.add_lt_top {a b : ℕ∞} :
            a + b < a < b <
            @[simp]
            theorem ENat.lift_add (a b : ℕ∞) (h : a + b < ) :
            (a + b).lift h = a.lift + b.lift

            Conversion of ℕ∞ to sending to 0.

            Equations
              Instances For

                Homomorphism from ℕ∞ to sending to 0.

                Equations
                  Instances For
                    theorem ENat.toNatHom_apply (n : ) :
                    toNatHom n = (↑n).toNat
                    @[simp]
                    theorem ENat.toNat_coe (n : ) :
                    (↑n).toNat = n
                    @[simp]
                    theorem ENat.toNat_zero :
                    toNat 0 = 0
                    @[simp]
                    theorem ENat.toNat_one :
                    toNat 1 = 1
                    @[simp]
                    @[simp]
                    @[simp]
                    theorem ENat.toNat_eq_zero {n : ℕ∞} :
                    n.toNat = 0 n = 0 n =
                    theorem ENat.lift_eq_toNat_of_lt_top {x : ℕ∞} (hx : x < ) :
                    x.lift hx = x.toNat
                    @[simp]
                    theorem ENat.recTopCoe_zero {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
                    recTopCoe d f 0 = f 0
                    @[simp]
                    theorem ENat.recTopCoe_one {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
                    recTopCoe d f 1 = f 1
                    @[simp]
                    theorem ENat.recTopCoe_ofNat {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) (x : ) [x.AtLeastTwo] :
                    @[simp]
                    theorem ENat.top_ne_coe (a : ) :
                    a
                    @[simp]
                    @[simp]
                    @[simp]
                    theorem ENat.coe_ne_top (a : ) :
                    a
                    @[simp]
                    @[simp]
                    @[simp]
                    theorem ENat.top_sub_coe (a : ) :
                    - a =
                    @[simp]
                    @[simp]
                    theorem ENat.top_pos :
                    0 <
                    @[deprecated ENat.top_pos (since := "2024-10-22")]

                    Alias of ENat.top_pos.

                    @[simp]
                    theorem ENat.one_lt_top :
                    1 <
                    @[simp]
                    theorem ENat.sub_top (a : ℕ∞) :
                    a - = 0
                    @[simp]
                    theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
                    n.toNat = n n
                    theorem ENat.coe_toNat {n : ℕ∞} :
                    n n.toNat = n

                    Alias of the reverse direction of ENat.coe_toNat_eq_self.

                    @[simp]
                    theorem ENat.toNat_eq_iff_eq_coe (n : ℕ∞) (m : ) [NeZero m] :
                    n.toNat = m n = m
                    theorem ENat.toNat_add {m n : ℕ∞} (hm : m ) (hn : n ) :
                    (m + n).toNat = m.toNat + n.toNat
                    theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
                    (m - n).toNat = m.toNat - n.toNat
                    @[simp]
                    theorem ENat.toNat_mul (a b : ℕ∞) :
                    (a * b).toNat = a.toNat * b.toNat
                    theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
                    m.toNat = n m = n
                    theorem ENat.toNat_le_of_le_coe {m : ℕ∞} {n : } (h : m n) :
                    theorem ENat.toNat_le_toNat {m n : ℕ∞} (h : m n) (hn : n ) :
                    @[simp]
                    theorem ENat.succ_def (m : ℕ∞) :
                    Order.succ m = m + 1
                    theorem ENat.add_one_le_iff {m n : ℕ∞} (hm : m ) :
                    m + 1 n m < n
                    theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :
                    n < 1 n = 0
                    theorem ENat.lt_add_one_iff {m n : ℕ∞} (hm : n ) :
                    m < n + 1 m n
                    theorem ENat.lt_coe_add_one_iff {m : ℕ∞} {n : } :
                    m < n + 1 m n
                    theorem ENat.le_coe_iff {n : ℕ∞} {k : } :
                    n k ∃ (n₀ : ), n = n₀ n₀ k
                    @[simp]
                    theorem ENat.not_lt_zero (n : ℕ∞) :
                    ¬n < 0
                    @[simp]
                    theorem ENat.coe_lt_top (n : ) :
                    n <
                    theorem ENat.coe_lt_coe {n m : } :
                    n < m n < m
                    theorem ENat.coe_le_coe {n m : } :
                    n m n m
                    theorem ENat.nat_induction {P : ℕ∞Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ), P nP n.succ) (htop : (∀ (n : ), P n)P ) :
                    P a
                    theorem ENat.add_one_pos {n : ℕ∞} :
                    0 < n + 1
                    theorem ENat.add_lt_add_iff_right {m n k : ℕ∞} (h : k ) :
                    n + k < m + k n < m
                    theorem ENat.add_lt_add_iff_left {m n k : ℕ∞} (h : k ) :
                    k + n < k + m n < m
                    theorem ENat.ne_top_iff_exists {n : ℕ∞} :
                    n ∃ (m : ), m = n
                    theorem ENat.eq_top_iff_forall_ne {n : ℕ∞} :
                    n = ∀ (m : ), m n
                    theorem ENat.eq_top_iff_forall_gt {n : ℕ∞} :
                    n = ∀ (m : ), m < n
                    theorem ENat.eq_top_iff_forall_ge {n : ℕ∞} :
                    n = ∀ (m : ), m n
                    theorem ENat.forall_natCast_le_iff_le {m n : ℕ∞} :
                    (∀ (a : ), a ma n) m n

                    Version of WithTop.forall_coe_le_iff_le using Nat.cast rather than WithTop.some.

                    theorem ENat.eq_of_forall_natCast_le_iff {m n : ℕ∞} (hm : ∀ (a : ), a m a n) :
                    m = n

                    Version of WithTop.eq_of_forall_coe_le_iff using Nat.cast rather than WithTop.some.

                    theorem ENat.exists_nat_gt {n : ℕ∞} (hn : n ) :
                    ∃ (m : ), n < m
                    @[simp]
                    theorem ENat.sub_eq_top_iff {a b : ℕ∞} :
                    a - b = a = b
                    theorem ENat.le_sub_of_add_le_left {a b c : ℕ∞} (ha : a ) :
                    a + b cb c - a
                    theorem ENat.sub_sub_cancel {a b : ℕ∞} (h : a ) (h2 : b a) :
                    a - (a - b) = b
                    theorem ENat.mul_left_strictMono {a : ℕ∞} (ha : a 0) (h_top : a ) :
                    StrictMono fun (x : ℕ∞) => a * x
                    theorem ENat.mul_right_strictMono {a : ℕ∞} (ha : a 0) (h_top : a ) :
                    StrictMono fun (x : ℕ∞) => x * a
                    @[simp]
                    theorem ENat.mul_le_mul_left_iff {a x y : ℕ∞} (ha : a 0) (h_top : a ) :
                    a * x a * y x y
                    @[simp]
                    theorem ENat.mul_le_mul_right_iff {a x y : ℕ∞} (ha : a 0) (h_top : a ) :
                    x * a y * a x y
                    theorem ENat.mul_le_mul_of_le_right {a x y : ℕ∞} (hxy : x y) (ha : a 0) (h_top : a ) :
                    x * a y * a
                    theorem ENat.self_le_mul_right {c : ℕ∞} (a : ℕ∞) (hc : c 0) :
                    a a * c
                    theorem ENat.self_le_mul_left {c : ℕ∞} (a : ℕ∞) (hc : c 0) :
                    a c * a
                    theorem ENat.add_one_natCast_le_withTop_of_lt {m : } {n : WithTop ℕ∞} (h : m < n) :
                    ↑(m + 1) n
                    @[simp]
                    theorem ENat.coe_top_add_one :
                    + 1 =
                    @[simp]
                    theorem ENat.add_one_eq_coe_top_iff {n : WithTop ℕ∞} :
                    n + 1 = n =
                    @[simp]
                    theorem ENat.natCast_ne_coe_top (n : ) :
                    n
                    @[deprecated ENat.natCast_ne_coe_top (since := "2024-10-22")]
                    theorem ENat.nat_ne_coe_top (n : ) :
                    n

                    Alias of ENat.natCast_ne_coe_top.

                    theorem ENat.natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : N) (n : ) :
                    n N
                    theorem ENat.natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : N) (n : ) :
                    n < N
                    def ENat.map {α : Type u_1} (f : α) (k : ℕ∞) :

                    Specialization of WithTop.map to ENat.

                    Equations
                      Instances For
                        @[simp]
                        theorem ENat.map_top {α : Type u_1} (f : α) :
                        @[simp]
                        theorem ENat.map_coe {α : Type u_1} (f : α) (a : ) :
                        map f a = (f a)
                        @[simp]
                        theorem ENat.map_zero {α : Type u_1} (f : α) :
                        map f 0 = (f 0)
                        @[simp]
                        theorem ENat.map_one {α : Type u_1} (f : α) :
                        map f 1 = (f 1)
                        @[simp]
                        theorem ENat.map_ofNat {α : Type u_1} (f : α) (n : ) [n.AtLeastTwo] :
                        map f (OfNat.ofNat n) = (f n)
                        @[simp]
                        theorem ENat.map_eq_top_iff {n : ℕ∞} {α : Type u_1} {f : α} :
                        map f n = n =
                        @[simp]
                        theorem ENat.strictMono_map_iff {α : Type u_1} {f : α} [Preorder α] :
                        @[simp]
                        theorem ENat.monotone_map_iff {α : Type u_1} {f : α} [Preorder α] :
                        @[simp]
                        @[simp]
                        @[simp]
                        theorem ENat.map_add {β : Type u_2} {F : Type u_3} [Add β] [FunLike F β] [AddHomClass F β] (f : F) (a b : ℕ∞) :
                        map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b
                        def OneHom.ENatMap {N : Type u_2} [One N] (f : OneHom N) :

                        A version of ENat.map for OneHoms.

                        Equations
                          Instances For
                            def ZeroHom.ENatMap {N : Type u_2} [Zero N] (f : ZeroHom N) :

                            A version of ENat.map for ZeroHoms.

                            Equations
                              Instances For
                                def AddHom.ENatMap {N : Type u_2} [Add N] (f : →ₙ+ N) :

                                A version of WithTop.map for AddHoms.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem AddHom.ENatMap_apply {N : Type u_2} [Add N] (f : →ₙ+ N) :
                                    f.ENatMap = ENat.map f

                                    A version of WithTop.map for AddMonoidHoms.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem AddMonoidHom.ENatMap_apply {N : Type u_2} [AddZeroClass N] (f : →+ N) :
                                        f.ENatMap = ENat.map f

                                        A version of ENat.map for MonoidWithZeroHoms.

                                        Equations
                                          Instances For
                                            @[simp]

                                            A version of ENat.map for RingHoms.

                                            Equations
                                              Instances For
                                                theorem WithBot.lt_add_one_iff {n : WithBot ℕ∞} {m : } :
                                                n < m + 1 n m
                                                theorem WithBot.add_one_le_iff {n : } {m : WithBot ℕ∞} :
                                                n + 1 m n < m