The type of nonnegative elements

This file defines instances and prove some properties about the nonnegative elements Nonneg α 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.

@[reducible, inline]

abbrev Nonneg (α : Type u_2) [Zero α] [LE α] : Type u_2

The subtype of nonnegative elements.

TODO: Nonneg could be converted to a one-field or two-field structure, as discussed on Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/near/585745328

Equations

• Nonneg α = { x : α // 0 ≤ x }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Nonneg.zero {α : Type u_1} [Zero α] [Preorder α] : Zero (Nonneg α)

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_reducible]

instance Nonneg.add {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] : Add (Nonneg α)

Equations

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

@[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, ⋯⟩

@[simp]

theorem Nonneg.coe_add {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] (a b : Nonneg α) : ↑(a + b) = ↑a + ↑b

instance Nonneg.instIsLeftCancelAdd {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsLeftCancelAdd α] : IsLeftCancelAdd (Nonneg α)

instance Nonneg.instIsRightCancelAdd {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsRightCancelAdd α] : IsRightCancelAdd (Nonneg α)

instance Nonneg.instIsCancelAdd {α : Type u_1} [AddZeroClass α] [Preorder α] [AddLeftMono α] [IsCancelAdd α] : IsCancelAdd (Nonneg α)

@[instance_reducible]

instance Nonneg.nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] : SMul ℕ (Nonneg α)

Equations

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

@[simp]

theorem Nonneg.nsmul_mk {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x) : n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩

@[simp]

theorem Nonneg.coe_nsmul {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) (a : Nonneg α) : ↑(n • a) = n • ↑a

@[instance_reducible]

instance Nonneg.one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] : One (Nonneg α)

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_reducible]

instance Nonneg.mul {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] : Mul (Nonneg α)

Equations

• Nonneg.mul = { mul := fun (x y : Nonneg α) => ⟨↑x * ↑y, ⋯⟩ }

@[simp]

theorem Nonneg.coe_mul {α : Type u_1} [MulZeroClass α] [Preorder α] [PosMulMono α] (a b : Nonneg α) : ↑(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_reducible]

instance Nonneg.addMonoid {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] : AddMonoid (Nonneg α)

Equations

• Nonneg.addMonoid = { toZero := Nonneg.zero, toAdd := Nonneg.add, add_assoc := ⋯, zero_add := ⋯, add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }

def Nonneg.coeAddMonoidHom {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] : Nonneg α →+ α

Coercion Nonneg α → α as an AddMonoidHom.

Equations

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

@[simp]

theorem Nonneg.coeAddMonoidHom_apply {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (self : { x : α // 0 ≤ x }) : coeAddMonoidHom self = ↑self

theorem Nonneg.nsmul_coe {α : Type u_1} [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) (r : Nonneg α) : ↑(n • r) = n • ↑r

@[instance_reducible]

instance Nonneg.addCommMonoid {α : Type u_1} [AddCommMonoid α] [Preorder α] [AddLeftMono α] : AddCommMonoid (Nonneg α)

Equations

• Nonneg.addCommMonoid = { toAddMonoid := Nonneg.addMonoid, add_comm := ⋯ }

@[instance_reducible]

instance Nonneg.addCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] [Preorder α] [AddLeftMono α] : AddCancelCommMonoid (Nonneg α)

Equations

• Nonneg.addCancelCommMonoid = { toAddCommMonoid := Nonneg.addCommMonoid, toIsLeftCancelAdd := ⋯ }

@[instance_reducible]

instance Nonneg.natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] : NatCast (Nonneg α)

Equations

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

@[simp]

theorem Nonneg.coe_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Nonneg.mk_natCast {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] (n : ℕ) : ⟨↑n, ⋯⟩ = ↑n

@[instance_reducible]

instance Nonneg.addMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] : AddMonoidWithOne (Nonneg α)

Equations

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

@[instance_reducible]

instance Nonneg.pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] : Pow (Nonneg α) ℕ

Equations

• Nonneg.pow = { pow := fun (x : Nonneg α) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

@[simp]

theorem Nonneg.coe_pow {α : Type u_1} [MonoidWithZero α] [Preorder α] [ZeroLEOneClass α] [PosMulMono α] (a : Nonneg α) (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_reducible]

instance Nonneg.semiring {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] : Semiring (Nonneg α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Nonneg.monoidWithZero {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] : MonoidWithZero (Nonneg α)

Equations

• Nonneg.monoidWithZero = inferInstance

def Nonneg.coeRingHom {α : Type u_1} [Semiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] : Nonneg α →+* α

Coercion Nonneg α → α as a RingHom.

Equations

• Nonneg.coeRingHom = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

instance Nonneg.commSemiring {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] : CommSemiring (Nonneg α)

Equations

• Nonneg.commSemiring = { toSemiring := Nonneg.semiring, mul_comm := ⋯ }

@[instance_reducible]

instance Nonneg.commMonoidWithZero {α : Type u_1} [CommSemiring α] [PartialOrder α] [ZeroLEOneClass α] [AddLeftMono α] [PosMulMono α] : CommMonoidWithZero (Nonneg α)

Equations

• Nonneg.commMonoidWithZero = inferInstance

def Nonneg.toNonneg {α : Type u_1} [Zero α] [SemilatticeSup α] (a : α) : Nonneg α

The function a ↦ max a 0 of type α → Nonneg α.

Equations

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

@[simp]

theorem Nonneg.coe_toNonneg {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} : ↑(toNonneg a) = a ⊔ 0

@[simp]

theorem Nonneg.toNonneg_of_nonneg {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} (h : 0 ≤ a) : toNonneg a = ⟨a, h⟩

@[simp]

theorem Nonneg.toNonneg_coe {α : Type u_1} [Zero α] [SemilatticeSup α] {a : Nonneg α} : toNonneg ↑a = a

@[simp]

theorem Nonneg.toNonneg_le {α : Type u_1} [Zero α] [SemilatticeSup α] {a : α} {b : Nonneg α} : toNonneg a ≤ b ↔ a ≤ ↑b

@[instance_reducible]

instance Nonneg.sub {α : Type u_1} [Zero α] [SemilatticeSup α] [Sub α] : Sub (Nonneg α)

Equations

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

@[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)

@[simp]

theorem Nonneg.toNonneg_lt {α : Type u_1} [Zero α] [LinearOrder α] {a : Nonneg α} {b : α} : a < toNonneg b ↔ ↑a < b