Documentation

Mathlib.Algebra.Order.Ring.Unbundled.Nonneg

The type of nonnegative elements #

This file defines instances and prove some properties about the nonnegative elements {x : α // 0 ≤ x} of an arbitrary type α.

Currently we only state instances and states some simp/norm_cast lemmas.

When α is , this will give us some properties about ℝ≥0.

Implementation Notes #

Instead of {x : α // 0 ≤ x} we could also use Set.Ici (0 : α), which is definitionally equal. However, using the explicit subtype has a big advantage: when writing an element explicitly with a proof of nonnegativity as ⟨x, hx⟩, the hx is expected to have type 0 ≤ x. If we would use Ici 0, then the type is expected to be x ∈ Ici 0. Although these types are definitionally equal, this often confuses the elaborator. Similar problems arise when doing cases on an element.

The disadvantage is that we have to duplicate some instances about Set.Ici to this subtype.

instance Nonneg.orderBot {α : Type u_1} [Preorder α] {a : α} :
OrderBot { x : α // a x }

This instance uses data fields from Subtype.partialOrder to help type-class inference. The Set.Ici data fields are definitionally equal, but that requires unfolding semireducible definitions, so type-class inference won't see this.

Equations
theorem Nonneg.bot_eq {α : Type u_1} [Preorder α] {a : α} :
= a,
instance Nonneg.noMaxOrder {α : Type u_1} [PartialOrder α] [NoMaxOrder α] {a : α} :
NoMaxOrder { x : α // a x }
Equations
  • =
instance Nonneg.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
SemilatticeSup { x : α // a x }
Equations
  • Nonneg.semilatticeSup = Set.Ici.semilatticeSup
instance Nonneg.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
SemilatticeInf { x : α // a x }
Equations
  • Nonneg.semilatticeInf = Set.Ici.semilatticeInf
instance Nonneg.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
DistribLattice { x : α // a x }
Equations
  • Nonneg.distribLattice = Set.Ici.distribLattice
instance Nonneg.instDenselyOrdered {α : Type u_1} [Preorder α] [DenselyOrdered α] {a : α} :
DenselyOrdered { x : α // a x }
Equations
  • =
@[reducible, inline]

If sSup ∅ ≤ a then {x : α // a ≤ x} is a ConditionallyCompleteLinearOrder.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline]

    If sSup ∅ ≤ a then {x : α // a ≤ x} is a ConditionallyCompleteLinearOrderBot.

    This instance uses data fields from Subtype.linearOrder to help type-class inference. The Set.Ici data fields are definitionally equal, but that requires unfolding semireducible definitions, so type-class inference won't see this.

    Equations
    Instances For
      instance Nonneg.inhabited {α : Type u_1} [Preorder α] {a : α} :
      Inhabited { x : α // a x }
      Equations
      • Nonneg.inhabited = { default := a, }
      instance Nonneg.zero {α : Type u_1} [Zero α] [Preorder α] :
      Zero { x : α // 0 x }
      Equations
      • Nonneg.zero = { zero := 0, }
      @[simp]
      theorem Nonneg.coe_zero {α : Type u_1} [Zero α] [Preorder α] :
      0 = 0
      @[simp]
      theorem Nonneg.mk_eq_zero {α : Type u_1} [Zero α] [Preorder α] {x : α} (hx : 0 x) :
      x, hx = 0 x = 0
      instance Nonneg.add {α : Type u_1} [AddZeroClass α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
      Add { x : α // 0 x }
      Equations
      • Nonneg.add = { add := fun (x y : { x : α // 0 x }) => x + y, }
      @[simp]
      theorem Nonneg.mk_add_mk {α : Type u_1} [AddZeroClass α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {x : α} {y : α} (hx : 0 x) (hy : 0 y) :
      x, hx + y, hy = x + y,
      @[simp]
      theorem Nonneg.coe_add {α : Type u_1} [AddZeroClass α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : { x : α // 0 x }) (b : { x : α // 0 x }) :
      (a + b) = a + b
      instance Nonneg.nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
      SMul { x : α // 0 x }
      Equations
      • Nonneg.nsmul = { smul := fun (n : ) (x : { x : α // 0 x }) => n x, }
      @[simp]
      theorem Nonneg.nsmul_mk {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (n : ) {x : α} (hx : 0 x) :
      n x, hx = n x,
      @[simp]
      theorem Nonneg.coe_nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (n : ) (a : { x : α // 0 x }) :
      (n a) = n a
      instance Nonneg.one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
      One { x : α // 0 x }
      Equations
      • Nonneg.one = { one := 1, }
      @[simp]
      theorem Nonneg.coe_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
      1 = 1
      @[simp]
      theorem Nonneg.mk_eq_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] {x : α} (hx : 0 x) :
      x, hx = 1 x = 1
      instance Nonneg.mul {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] :
      Mul { x : α // 0 x }
      Equations
      • Nonneg.mul = { mul := fun (x y : { x : α // 0 x }) => x * y, }
      @[simp]
      theorem Nonneg.coe_mul {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] (a : { x : α // 0 x }) (b : { x : α // 0 x }) :
      (a * b) = a * b
      @[simp]
      theorem Nonneg.mk_mul_mk {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] {x : α} {y : α} (hx : 0 x) (hy : 0 y) :
      x, hx * y, hy = x * y,
      instance Nonneg.addMonoid {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
      AddMonoid { x : α // 0 x }
      Equations
      def Nonneg.coeAddMonoidHom {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
      { x : α // 0 x } →+ α

      Coercion {x : α // 0 ≤ x} → α as an AddMonoidHom.

      Equations
      • Nonneg.coeAddMonoidHom = { toFun := Subtype.val, map_zero' := , map_add' := }
      Instances For
        theorem Nonneg.nsmul_coe {α : Type u_1} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (n : ) (r : { x : α // 0 x }) :
        (n r) = n r
        instance Nonneg.addCommMonoid {α : Type u_1} [AddCommMonoid α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
        AddCommMonoid { x : α // 0 x }
        Equations
        instance Nonneg.natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] :
        NatCast { x : α // 0 x }
        Equations
        • Nonneg.natCast = { natCast := fun (n : ) => n, }
        @[simp]
        theorem Nonneg.coe_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] (n : ) :
        n = n
        @[deprecated Nonneg.coe_natCast]
        theorem Nonneg.coe_nat_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] (n : ) :
        n = n

        Alias of Nonneg.coe_natCast.

        @[simp]
        theorem Nonneg.mk_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] (n : ) :
        n, = n
        @[deprecated Nonneg.mk_natCast]
        theorem Nonneg.mk_nat_cast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] (n : ) :
        n, = n

        Alias of Nonneg.mk_natCast.

        instance Nonneg.addMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [ZeroLEOneClass α] :
        AddMonoidWithOne { x : α // 0 x }
        Equations
        @[simp]
        theorem Nonneg.pow_nonneg {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] {a : α} (H : 0 a) (n : ) :
        0 a ^ n
        instance Nonneg.pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] :
        Pow { x : α // 0 x }
        Equations
        • Nonneg.pow = { pow := fun (x : { x : α // 0 x }) (n : ) => x ^ n, }
        @[simp]
        theorem Nonneg.coe_pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] (a : { x : α // 0 x }) (n : ) :
        (a ^ n) = a ^ n
        @[simp]
        theorem Nonneg.mk_pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] {x : α} (hx : 0 x) (n : ) :
        x, hx ^ n = x ^ n,
        instance Nonneg.semiring {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [PosMulMono α] :
        Semiring { x : α // 0 x }
        Equations
        instance Nonneg.monoidWithZero {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [PosMulMono α] :
        MonoidWithZero { x : α // 0 x }
        Equations
        • Nonneg.monoidWithZero = inferInstance
        def Nonneg.coeRingHom {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [PosMulMono α] :
        { x : α // 0 x } →+* α

        Coercion {x : α // 0 ≤ x} → α as a RingHom.

        Equations
        • Nonneg.coeRingHom = { toFun := Subtype.val, map_one' := , map_mul' := , map_zero' := , map_add' := }
        Instances For
          instance Nonneg.commSemiring {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [PosMulMono α] :
          CommSemiring { x : α // 0 x }
          Equations
          instance Nonneg.commMonoidWithZero {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [PosMulMono α] :
          CommMonoidWithZero { x : α // 0 x }
          Equations
          • Nonneg.commMonoidWithZero = inferInstance
          def Nonneg.toNonneg {α : Type u_1} [Zero α] [LinearOrder α] (a : α) :
          { x : α // 0 x }

          The function a ↦ max a 0 of type α → {x : α // 0 ≤ x}.

          Equations
          Instances For
            @[simp]
            theorem Nonneg.coe_toNonneg {α : Type u_1} [Zero α] [LinearOrder α] {a : α} :
            (Nonneg.toNonneg a) = max a 0
            @[simp]
            theorem Nonneg.toNonneg_of_nonneg {α : Type u_1} [Zero α] [LinearOrder α] {a : α} (h : 0 a) :
            Nonneg.toNonneg a = a, h
            @[simp]
            theorem Nonneg.toNonneg_coe {α : Type u_1} [Zero α] [LinearOrder α] {a : { x : α // 0 x }} :
            @[simp]
            theorem Nonneg.toNonneg_le {α : Type u_1} [Zero α] [LinearOrder α] {a : α} {b : { x : α // 0 x }} :
            @[simp]
            theorem Nonneg.toNonneg_lt {α : Type u_1} [Zero α] [LinearOrder α] {a : { x : α // 0 x }} {b : α} :
            a < Nonneg.toNonneg b a < b
            instance Nonneg.sub {α : Type u_1} [Zero α] [LinearOrder α] [Sub α] :
            Sub { x : α // 0 x }
            Equations
            @[simp]
            theorem Nonneg.mk_sub_mk {α : Type u_1} [Zero α] [LinearOrder α] [Sub α] {x : α} {y : α} (hx : 0 x) (hy : 0 y) :
            x, hx - y, hy = Nonneg.toNonneg (x - y)