# 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.

source
instance Nonneg.inhabited {α : Type u_1} [Preorder α] {a : α} :
Inhabited { x : α // a ≤ x }
Equations

- Nonneg.inhabited = { default := ⟨a, ⋯⟩ }

source
instance Nonneg.zero {α : Type u_1} [Zero α] [Preorder α] :
Zero { x : α // 0 ≤ x }
Equations

- Nonneg.zero = { zero := ⟨0, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_zero {α : Type u_1} [Zero α] [Preorder α] :
↑0 = 0
source
@[simp]
theorem Nonneg.mk_eq_zero {α : Type u_1} [Zero α] [Preorder α] {x : α} (hx : 0 ≤ x) :
⟨x, hx⟩ = 0 ↔ x = 0
source
instance Nonneg.add {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] :
Add { x : α // 0 ≤ x }
Equations

- Nonneg.add = { add := fun (x y : { x : α // 0 ≤ x }) => ⟨↑x + ↑y, ⋯⟩ }

source
@[simp]
theorem Nonneg.mk_add_mk {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
source
@[simp]
theorem Nonneg.coe_add {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] (a b : { x : α // 0 ≤ x }) :
↑(a + b) = ↑a + ↑b
source
instance Nonneg.instIsLeftCancelAddSubtypeLeOfNat {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsLeftCancelAdd α] :
IsLeftCancelAdd { x : α // 0 ≤ x }
source
instance Nonneg.instIsRightCancelAddSubtypeLeOfNat {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsRightCancelAdd α] :
IsRightCancelAdd { x : α // 0 ≤ x }
source
instance Nonneg.instIsCancelAddSubtypeLeOfNat {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsCancelAdd α] :
IsCancelAdd { x : α // 0 ≤ x }
source
instance Nonneg.nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] :
SMul ℕ { x : α // 0 ≤ x }
Equations

- Nonneg.nsmul = { smul := fun (n : ℕ) (x : { x : α // 0 ≤ x }) => ⟨n • ↑x, ⋯⟩ }

source
@[simp]
theorem Nonneg.nsmul_mk {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x) :
n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩
source
@[simp]
theorem Nonneg.coe_nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) (a : { x : α // 0 ≤ x }) :
↑(n • a) = n • ↑a
source
instance Nonneg.one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
One { x : α // 0 ≤ x }
Equations

- Nonneg.one = { one := ⟨1, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
↑1 = 1
source
@[simp]
theorem Nonneg.mk_eq_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] {x : α} (hx : 0 ≤ x) :
⟨x, hx⟩ = 1 ↔ x = 1
source
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, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_mul {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] (a b : { x : α // 0 ≤ x }) :
↑(a * b) = ↑a * ↑b
source
@[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, ⋯⟩
source
instance Nonneg.addMonoid {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] :
AddMonoid { x : α // 0 ≤ x }
Equations

- Nonneg.addMonoid = Function.Injective.addMonoid (fun (a : { x : α // 0 ≤ x }) => ↑a) ⋯ ⋯ ⋯ ⋯

source
def Nonneg.coeAddMonoidHom {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] :
{ x : α // 0 ≤ x } →+ α

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

Equations

- Nonneg.coeAddMonoidHom = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Nonneg.coeAddMonoidHom_apply {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (self : { x : α // 0 ≤ x }) :
coeAddMonoidHom self = ↑self
source
theorem Nonneg.nsmul_coe {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) (r : { x : α // 0 ≤ x }) :
↑(n • r) = n • ↑r
source
instance Nonneg.addCommMonoid {α : Type u_1} [AddCommMonoid α] [Preorder α] [AddLeftMono α] :
AddCommMonoid { x : α // 0 ≤ x }
Equations

- Nonneg.addCommMonoid = Function.Injective.addCommMonoid (fun (a : { x : α // 0 ≤ x }) => ↑a) ⋯ ⋯ ⋯ ⋯

source
instance Nonneg.natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] :
NatCast { x : α // 0 ≤ x }
Equations

- Nonneg.natCast = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem Nonneg.mk_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) :
⟨↑n, ⋯⟩ = ↑n
source
instance Nonneg.addMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] :
AddMonoidWithOne { x : α // 0 ≤ x }
Equations

- Nonneg.addMonoidWithOne = { toNatCast := Nonneg.natCast, toAddMonoid := Nonneg.addMonoid, toOne := Nonneg.one, natCast_zero := ⋯, natCast_succ := ⋯ }

source
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, ⋯⟩ }

source
@[simp]
theorem Nonneg.coe_pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] (a : { x : α // 0 ≤ x }) (n : ℕ) :
↑(a ^ n) = ↑a ^ n
source
@[simp]
theorem Nonneg.mk_pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] {x : α} (hx : 0 ≤ x) (n : ℕ) :
⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
source
@[deprecated pow_nonneg (since := "2025-05-19")]
theorem Nonneg.pow_nonneg {M₀ : Type u_2} [MonoidWithZero M₀] [Preorder M₀] {a : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀] (ha : 0 ≤ a) (n : ℕ) :
0 ≤ a ^ n

Alias of `pow_nonneg`.

source
instance Nonneg.semiring {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] :
Semiring { x : α // 0 ≤ x }
Equations

- Nonneg.semiring = Function.Injective.semiring (fun (a : { x : α // 0 ≤ x }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source
instance Nonneg.monoidWithZero {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] :
MonoidWithZero { x : α // 0 ≤ x }
Equations

- Nonneg.monoidWithZero = inferInstance

source
def Nonneg.coeRingHom {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [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

source
instance Nonneg.commSemiring {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] :
CommSemiring { x : α // 0 ≤ x }
Equations

- Nonneg.commSemiring = Function.Injective.commSemiring (fun (a : { x : α // 0 ≤ x }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source
instance Nonneg.commMonoidWithZero {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] :
CommMonoidWithZero { x : α // 0 ≤ x }
Equations

- Nonneg.commMonoidWithZero = inferInstance

source
def Nonneg.toNonneg {α : Type u_1} [Zero α] [SemilatticeSup α] (a : α) :
{ x : α // 0 ≤ x }

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

Equations

- Nonneg.toNonneg a = ⟨a ⊔ 0, ⋯⟩

Instances For

source
@[simp]
theorem Nonneg.coe_toNonneg {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} :
↑(toNonneg a) = a ⊔ 0
source
@[simp]
theorem Nonneg.toNonneg_of_nonneg {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} (h : 0 ≤ a) :
toNonneg a = ⟨a, h⟩
source
@[simp]
theorem Nonneg.toNonneg_coe {α : Type u_1} [Zero α] [SemilatticeSup α] {a : { x : α // 0 ≤ x }} :
toNonneg ↑a = a
source
@[simp]
theorem Nonneg.toNonneg_le {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} {b : { x : α // 0 ≤ x }} :
toNonneg a ≤ b ↔ a ≤ ↑b
source
instance Nonneg.sub {α : Type u_1} [Zero α] [SemilatticeSup α] [Sub α] :
Sub { x : α // 0 ≤ x }
Equations

- Nonneg.sub = { sub := fun (x y : { x : α // 0 ≤ x }) => Nonneg.toNonneg (↑x - ↑y) }

source
@[simp]
theorem Nonneg.mk_sub_mk {α : Type u_1} [Zero α] [SemilatticeSup α] [Sub α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ - ⟨y, hy⟩ = toNonneg (x - y)
source
@[simp]
theorem Nonneg.toNonneg_lt {α : Type u_1} [Zero α] [LinearOrder α] {a : { x : α // 0 ≤ x }} {b : α} :
a < toNonneg b ↔ ↑a < b