doc-next-gen

Mathlib.Algebra.Order.Nonneg.Basic

Module docstring

{"# 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. "}

Nonneg.inhabited instance
[Preorder α] {a : α} : Inhabited { x : α // a ≤ x }
Full source 
instance inhabited [Preorder α] {a : α} : Inhabited { x : α // a ≤ x } :=
  ⟨⟨a, le_rfl⟩⟩
Nonnegative Subtype is Inhabited
Informal description
For any preorder $\alpha$ and element $a \in \alpha$, the subtype $\{x : \alpha \mid a \leq x\}$ is inhabited.
Nonneg.zero instance
[Zero α] [Preorder α] : Zero { x : α // 0 ≤ x }
Full source 
instance zero [Zero α] [Preorder α] : Zero { x : α // 0 ≤ x } :=
  ⟨⟨0, le_rfl⟩⟩
Zero Element in Nonnegative Subtype
Informal description
For any type $\alpha$ with a zero element and a preorder, the subtype $\{x : \alpha \mid 0 \leq x\}$ has a zero element given by $0$.
Nonneg.coe_zero theorem
[Zero α] [Preorder α] : ((0 : { x : α // 0 ≤ x }) : α) = 0
Full source 
@[simp, norm_cast]
protected theorem coe_zero [Zero α] [Preorder α] : ((0 : { x : α // 0 ≤ x }) : α) = 0 :=
  rfl
Embedding of Zero in Nonnegative Subtype Equals Zero
Informal description
For any type $\alpha$ with a zero element and a preorder, the canonical embedding of the zero element from the subtype $\{x : \alpha \mid 0 \leq x\}$ into $\alpha$ is equal to the zero element of $\alpha$, i.e., $\uparrow 0 = 0$.
Nonneg.mk_eq_zero theorem
[Zero α] [Preorder α] {x : α} (hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) = 0 ↔ x = 0
Full source 
@[simp]
theorem mk_eq_zero [Zero α] [Preorder α] {x : α} (hx : 0 ≤ x) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) = 0 ↔ x = 0 :=
  Subtype.ext_iff
Characterization of Zero in Nonnegative Subtype
Informal description
Let $\alpha$ be a type with a zero element and a preorder. For any element $x \in \alpha$ with $0 \leq x$, the element $\langle x, hx \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to the zero element of the subtype if and only if $x = 0$ in $\alpha$.
Nonneg.add instance
[AddZeroClass α] [Preorder α] [AddLeftMono α] : Add { x : α // 0 ≤ x }
Full source 
instance add [AddZeroClass α] [Preorder α] [AddLeftMono α] : Add { x : α // 0 ≤ x } :=
  ⟨fun x y => ⟨x + y, add_nonneg x.2 y.2⟩⟩
Addition on Nonnegative Elements
Informal description
For any type $\alpha$ equipped with an addition operation, a zero element, and a preorder such that addition is monotone in the left argument, the subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements inherits an addition operation.
Nonneg.mk_add_mk theorem
[AddZeroClass α] [Preorder α] [AddLeftMono α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) + ⟨y, hy⟩ = ⟨x + y, add_nonneg hx hy⟩
Full source 
@[simp]
theorem mk_add_mk [AddZeroClass α] [Preorder α] [AddLeftMono α] {x y : α}
    (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) + ⟨y, hy⟩ = ⟨x + y, add_nonneg hx hy⟩ :=
  rfl
Addition of Nonnegative Elements in Subtype
Informal description
Let $\alpha$ be a type equipped with an addition operation, a zero element, and a preorder such that addition is monotone in the left argument. For any elements $x, y \in \alpha$ with $0 \leq x$ and $0 \leq y$, the sum of the nonnegative elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to $\langle x + y, \text{add\_nonneg } hx \, hy \rangle$.
Nonneg.coe_add theorem
[AddZeroClass α] [Preorder α] [AddLeftMono α] (a b : { x : α // 0 ≤ x }) : ((a + b : { x : α // 0 ≤ x }) : α) = a + b
Full source 
@[simp, norm_cast]
protected theorem coe_add [AddZeroClass α] [Preorder α] [AddLeftMono α]
    (a b : { x : α // 0 ≤ x }) : ((a + b : { x : α // 0 ≤ x }) : α) = a + b :=
  rfl
Coercion of Sum of Nonnegative Elements Equals Sum of Coercions
Informal description
Let $\alpha$ be a type equipped with an addition operation, a zero element, and a preorder such that addition is monotone in the left argument. For any nonnegative elements $a, b \in \{x : \alpha \mid 0 \leq x\}$, the coercion of their sum in the subtype to $\alpha$ equals the sum of their coerced values, i.e., $(a + b : \alpha) = (a : \alpha) + (b : \alpha)$.
Nonneg.nsmul instance
[AddMonoid α] [Preorder α] [AddLeftMono α] : SMul ℕ { x : α // 0 ≤ x }
Full source 
instance nsmul [AddMonoid α] [Preorder α] [AddLeftMono α] : SMul ℕ { x : α // 0 ≤ x } :=
  ⟨fun n x => ⟨n • (x : α), nsmul_nonneg x.prop n⟩⟩
Natural Number Scalar Multiplication on Nonnegative Elements of an Additive Monoid
Informal description
For any additive monoid $\alpha$ with a preorder such that addition is monotone in the left argument, the subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements inherits a natural scalar multiplication operation by natural numbers, where $n \cdot \langle x, hx \rangle = \langle n \cdot x, \text{nsmul\_nonneg } hx \, n \rangle$.
Nonneg.nsmul_mk theorem
[AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α} (hx : 0 ≤ x) : (n • (⟨x, hx⟩ : { x : α // 0 ≤ x })) = ⟨n • x, nsmul_nonneg hx n⟩
Full source 
@[simp]
theorem nsmul_mk [AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) {x : α}
    (hx : 0 ≤ x) : (n • (⟨x, hx⟩ : { x : α // 0 ≤ x })) = ⟨n • x, nsmul_nonneg hx n⟩ :=
  rfl
Scalar Multiplication of Nonnegative Element Constructor
Informal description
Let $\alpha$ be an additive monoid with a preorder such that addition is monotone in the left argument. For any natural number $n$ and element $x \in \alpha$ with $0 \leq x$, the scalar multiplication of $n$ with the nonnegative element $\langle x, hx \rangle$ is equal to $\langle n \cdot x, \text{nsmul\_nonneg } hx \, n \rangle$, where $\text{nsmul\_nonneg } hx \, n$ is a proof that $0 \leq n \cdot x$.
Nonneg.coe_nsmul theorem
[AddMonoid α] [Preorder α] [AddLeftMono α] (n : ℕ) (a : { x : α // 0 ≤ x }) : ((n • a : { x : α // 0 ≤ x }) : α) = n • (a : α)
Full source 
@[simp, norm_cast]
protected theorem coe_nsmul [AddMonoid α] [Preorder α] [AddLeftMono α]
    (n : ℕ) (a : { x : α // 0 ≤ x }) : ((n • a : { x : α // 0 ≤ x }) : α) = n • (a : α) :=
  rfl
Embedding of Scalar Multiplication in Nonnegative Subtype: $\iota(n \cdot a) = n \cdot \iota(a)$
Informal description
Let $\alpha$ be an additive monoid with a preorder such that addition is monotone in the left argument. For any natural number $n$ and any nonnegative element $a \in \{x : \alpha \mid 0 \leq x\}$, the canonical embedding of the scalar multiple $n \cdot a$ in $\alpha$ equals the scalar multiple $n \cdot (a : \alpha)$ in $\alpha$.
Nonneg.one instance
: One { x : α // 0 ≤ x }
Full source 
instance one : One { x : α // 0 ≤ x } where
  one := ⟨1, zero_le_one⟩
One Element of Nonnegative Subtype
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ has a canonical one element, which is the same as the one element of $\alpha$.
Nonneg.coe_one theorem
: ((1 : { x : α // 0 ≤ x }) : α) = 1
Full source 
@[simp, norm_cast]
protected theorem coe_one : ((1 : { x : α // 0 ≤ x }) : α) = 1 :=
  rfl
Embedding of One in Nonnegative Subtype: $\iota(1) = 1$
Informal description
The canonical embedding of the multiplicative identity $1$ from the subtype $\{x : \alpha \mid 0 \leq x\}$ into $\alpha$ equals the multiplicative identity $1$ in $\alpha$.
Nonneg.mk_eq_one theorem
{x : α} (hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) = 1 ↔ x = 1
Full source 
@[simp]
theorem mk_eq_one {x : α} (hx : 0 ≤ x) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) = 1 ↔ x = 1 :=
  Subtype.ext_iff
Characterization of One in Nonnegative Subtype: $\langle x, hx \rangle = 1 \leftrightarrow x = 1$
Informal description
For any element $x$ of a type $\alpha$ with $0 \leq x$, the element $\langle x, hx \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ equals the multiplicative identity $1$ if and only if $x = 1$ in $\alpha$.
Nonneg.mul instance
: Mul { x : α // 0 ≤ x }
Full source 
instance mul : Mul { x : α // 0 ≤ x } where
  mul x y := ⟨x * y, mul_nonneg x.2 y.2⟩
Multiplication on Nonnegative Elements
Informal description
The subtype of nonnegative elements $\{x : \alpha \mid 0 \leq x\}$ of a type $\alpha$ is equipped with a multiplication operation inherited from $\alpha$.
Nonneg.coe_mul theorem
(a b : { x : α // 0 ≤ x }) : ((a * b : { x : α // 0 ≤ x }) : α) = a * b
Full source 
@[simp, norm_cast]
protected theorem coe_mul (a b : { x : α // 0 ≤ x }) :
    ((a * b : { x : α // 0 ≤ x }) : α) = a * b :=
  rfl
Embedding Preserves Multiplication of Nonnegative Elements
Informal description
For any two nonnegative elements $a$ and $b$ in $\{x : \alpha \mid 0 \leq x\}$, the canonical embedding of their product in $\alpha$ equals the product of their embeddings, i.e., $(a \cdot b) = a \cdot b$ where the left-hand side is interpreted in $\alpha$.
Nonneg.mk_mul_mk theorem
{x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) * ⟨y, hy⟩ = ⟨x * y, mul_nonneg hx hy⟩
Full source 
@[simp]
theorem mk_mul_mk {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) * ⟨y, hy⟩ = ⟨x * y, mul_nonneg hx hy⟩ :=
  rfl
Product of Nonnegative Elements in Subtype
Informal description
For any elements $x, y$ in a type $\alpha$ with $0 \leq x$ and $0 \leq y$, the product of the nonnegative elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to $\langle x \cdot y, \text{mul\_nonneg } hx hy \rangle$, where $\text{mul\_nonneg } hx hy$ is a proof that $0 \leq x \cdot y$.
Nonneg.addMonoid instance
: AddMonoid { x : α // 0 ≤ x }
Full source 
instance addMonoid : AddMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.addMonoid _ Nonneg.coe_zero (fun _ _ => rfl) fun _ _ => rfl
Additive Monoid Structure on Nonnegative Elements
Informal description
For any type $\alpha$ with an additive monoid structure and a preorder such that addition is monotone in the left argument, the subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements inherits an additive monoid structure.
Nonneg.coeAddMonoidHom definition
: { x : α // 0 ≤ x } →+ α
Full source 
/-- Coercion `{x : α // 0 ≤ x} → α` as an `AddMonoidHom`. -/
@[simps]
def coeAddMonoidHom : { x : α // 0 ≤ x }{ x : α // 0 ≤ x } →+ α :=
  { toFun := ((↑) : { x : α // 0 ≤ x } → α)
    map_zero' := Nonneg.coe_zero
    map_add' := Nonneg.coe_add }
Canonical inclusion of nonnegative elements as an additive monoid homomorphism
Informal description
The canonical additive monoid homomorphism from the subtype of nonnegative elements $\{x : \alpha \mid 0 \leq x\}$ to $\alpha$, which maps each nonnegative element to its underlying value in $\alpha$. This homomorphism preserves the additive structure, sending the zero element to zero and addition to addition.
Nonneg.nsmul_coe theorem
(n : ℕ) (r : { x : α // 0 ≤ x }) : ↑(n • r) = n • (r : α)
Full source 
@[norm_cast]
theorem nsmul_coe (n : ℕ) (r : { x : α // 0 ≤ x }) :
    ↑(n • r) = n • (r : α) :=
  Nonneg.coeAddMonoidHom.map_nsmul _ _
Canonical inclusion commutes with scalar multiplication for nonnegative elements
Informal description
For any natural number $n$ and any nonnegative element $r$ in a type $\alpha$ (i.e., $r \in \{x : \alpha \mid 0 \leq x\}$), the canonical inclusion map $\uparrow$ (from the subtype to $\alpha$) commutes with scalar multiplication by $n$. That is, $\uparrow(n \cdot r) = n \cdot \uparrow(r)$.
Nonneg.addCommMonoid instance
: AddCommMonoid { x : α // 0 ≤ x }
Full source 
instance addCommMonoid : AddCommMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.addCommMonoid _ Nonneg.coe_zero (fun _ _ => rfl) (fun _ _ => rfl)
Additive Commutative Monoid Structure on Nonnegative Elements
Informal description
For any type $\alpha$ with an additive commutative monoid structure and a preorder such that addition is monotone in the left argument, the subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements inherits an additive commutative monoid structure.
Nonneg.natCast instance
: NatCast { x : α // 0 ≤ x }
Full source 
instance natCast : NatCast { x : α // 0 ≤ x } :=
  ⟨fun n => ⟨n, Nat.cast_nonneg' n⟩⟩
Natural Number Embedding for Nonnegative Elements
Informal description
For any type $\alpha$ with a partial order and a zero element, the subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements has a canonical `NatCast` structure, meaning it inherits the natural number embedding from $\alpha$.
Nonneg.coe_natCast theorem
(n : ℕ) : ((↑n : { x : α // 0 ≤ x }) : α) = n
Full source 
@[simp, norm_cast]
protected theorem coe_natCast (n : ℕ) : ((↑n : { x : α // 0 ≤ x }) : α) = n :=
  rfl
Coercion of Natural Numbers into Nonnegative Subtype Preserves Value
Informal description
For any natural number $n$, the canonical embedding of $n$ into the subtype of nonnegative elements of $\alpha$ (i.e., $\{x : \alpha \mid 0 \leq x\}$) is equal to $n$ when viewed as an element of $\alpha$. In other words, the coercion map satisfies $\uparrow n = n$ in $\alpha$.
Nonneg.mk_natCast theorem
(n : ℕ) : (⟨n, n.cast_nonneg'⟩ : { x : α // 0 ≤ x }) = n
Full source 
@[simp]
theorem mk_natCast (n : ℕ) : (⟨n, n.cast_nonneg'⟩ : { x : α // 0 ≤ x }) = n :=
  rfl
Canonical Embedding of Natural Numbers in Nonnegative Subtype
Informal description
For any natural number $n$, the element $\langle n, 0 \leq n \rangle$ in the subtype of nonnegative elements of $\alpha$ is equal to the canonical embedding of $n$ in $\alpha$.
Nonneg.addMonoidWithOne instance
: AddMonoidWithOne { x : α // 0 ≤ x }
Full source 
instance addMonoidWithOne : AddMonoidWithOne { x : α // 0 ≤ x } :=
  { Nonneg.one (α := α) with
    toNatCast := Nonneg.natCast
    natCast_zero := by ext; simp
    natCast_succ := fun _ => by ext; simp }
Additive Monoid with One Structure on Nonnegative Elements
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ inherits an additive monoid with one structure from $\alpha$. This means it has a zero element, an addition operation, and a one element, all satisfying the usual monoid axioms, with the additional property that all elements are nonnegative.
Nonneg.pow_nonneg theorem
{a : α} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ a ^ n
Full source 
@[simp]
theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ a ^ n
  | 0 => by
    rw [pow_zero]
    exact zero_le_one
  | n + 1 => by
    rw [pow_succ]
    exact mul_nonneg (pow_nonneg H _) H
Nonnegativity of Powers: $0 \leq a \implies \forall n \in \mathbb{N}, 0 \leq a^n$
Informal description
For any element $a$ in a type $\alpha$ with $0 \leq a$, and for any natural number $n$, the $n$-th power $a^n$ is also nonnegative, i.e., $0 \leq a^n$.
Nonneg.pow instance
: Pow { x : α // 0 ≤ x } ℕ
Full source 
instance pow : Pow { x : α // 0 ≤ x } ℕ where
  pow x n := ⟨(x : α) ^ n, pow_nonneg x.2 n⟩
Natural Power Operation on Nonnegative Elements
Informal description
For any type $\alpha$ with a nonnegative subset $\{x : \alpha \mid 0 \leq x\}$, there is a natural power operation defined on this subset, where for any nonnegative element $a$ and natural number $n$, the power $a^n$ is also nonnegative.
Nonneg.coe_pow theorem
(a : { x : α // 0 ≤ x }) (n : ℕ) : (↑(a ^ n) : α) = (a : α) ^ n
Full source 
@[simp, norm_cast]
protected theorem coe_pow (a : { x : α // 0 ≤ x }) (n : ℕ) :
    (↑(a ^ n) : α) = (a : α) ^ n :=
  rfl
Canonical Embedding Preserves Powers of Nonnegative Elements
Informal description
For any nonnegative element $a$ in a type $\alpha$ (i.e., $a \in \{x : \alpha \mid 0 \leq x\}$) and any natural number $n$, the canonical embedding of $a^n$ into $\alpha$ equals the $n$-th power of the canonical embedding of $a$ in $\alpha$. In other words, if $a$ is represented as $\langle x, h_x \rangle$ where $h_x$ is a proof that $0 \leq x$, then $(a^n : \alpha) = (a : \alpha)^n$.
Nonneg.mk_pow theorem
{x : α} (hx : 0 ≤ x) (n : ℕ) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, pow_nonneg hx n⟩
Full source 
@[simp]
theorem mk_pow {x : α} (hx : 0 ≤ x) (n : ℕ) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, pow_nonneg hx n⟩ :=
  rfl
Power of Nonnegative Element Preserves Nonnegativity
Informal description
For any element $x$ in a type $\alpha$ with $0 \leq x$ and any natural number $n$, the $n$-th power of the nonnegative element $\langle x, hx \rangle$ is equal to $\langle x^n, h \rangle$, where $h$ is a proof that $0 \leq x^n$.
Nonneg.semiring instance
: Semiring { x : α // 0 ≤ x }
Full source 
instance semiring : Semiring { x : α // 0 ≤ x } :=
  Subtype.coe_injective.semiring _ Nonneg.coe_zero Nonneg.coe_one
    (fun _ _ => rfl) (fun _ _=> rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ => rfl
Semiring Structure on Nonnegative Elements
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ forms a semiring, where the addition and multiplication operations are inherited from $\alpha$.
Nonneg.monoidWithZero instance
: MonoidWithZero { x : α // 0 ≤ x }
Full source 
instance monoidWithZero : MonoidWithZero { x : α // 0 ≤ x } := by infer_instance
Monoid with Zero Structure on Nonnegative Elements
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ forms a monoid with zero, where the multiplication and zero operations are inherited from $\alpha$.
Nonneg.coeRingHom definition
: { x : α // 0 ≤ x } →+* α
Full source 
/-- Coercion `{x : α // 0 ≤ x} → α` as a `RingHom`. -/
def coeRingHom : { x : α // 0 ≤ x }{ x : α // 0 ≤ x } →+* α :=
  { toFun := ((↑) : { x : α // 0 ≤ x } → α)
    map_one' := Nonneg.coe_one
    map_mul' := Nonneg.coe_mul
    map_zero' := Nonneg.coe_zero,
    map_add' := Nonneg.coe_add }
Canonical ring homomorphism from nonnegative elements
Informal description
The canonical ring homomorphism from the semiring of nonnegative elements $\{x \in \alpha \mid 0 \leq x\}$ to $\alpha$, which maps each nonnegative element to its underlying value in $\alpha$. This homomorphism preserves the additive and multiplicative structures, including the zero and one elements.
Nonneg.commSemiring instance
: CommSemiring { x : α // 0 ≤ x }
Full source 
instance commSemiring : CommSemiring { x : α // 0 ≤ x } :=
  Subtype.coe_injective.commSemiring _ Nonneg.coe_zero Nonneg.coe_one
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ => rfl
Commutative Semiring Structure on Nonnegative Elements
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ forms a commutative semiring, inheriting the addition and multiplication operations from $\alpha$ and satisfying all the axioms of a commutative semiring.
Nonneg.commMonoidWithZero instance
: CommMonoidWithZero { x : α // 0 ≤ x }
Full source 
instance commMonoidWithZero : CommMonoidWithZero { x : α // 0 ≤ x } := inferInstance
Commutative Monoid with Zero Structure on Nonnegative Elements
Informal description
The subtype $\{x : \alpha \mid 0 \leq x\}$ of nonnegative elements of a type $\alpha$ forms a commutative monoid with zero, inheriting the multiplication and zero elements from $\alpha$ and satisfying all the axioms of a commutative monoid with zero.
Nonneg.toNonneg definition
(a : α) : { x : α // 0 ≤ x }
Full source 
/-- The function `a ↦ max a 0` of type `α → {x : α // 0 ≤ x}`. -/
def toNonneg (a : α) : { x : α // 0 ≤ x } :=
  ⟨max a 0, le_sup_right⟩
Canonical map to nonnegative elements
Informal description
The function maps an element $a$ of type $\alpha$ to the pair $\langle \max(a, 0), h \rangle$ where $h$ is a proof that $0 \leq \max(a, 0)$. This defines a canonical map from $\alpha$ to the subtype of nonnegative elements $\{x : \alpha \mid 0 \leq x\}$.
Nonneg.coe_toNonneg theorem
{a : α} : (toNonneg a : α) = max a 0
Full source 
@[simp]
theorem coe_toNonneg {a : α} : (toNonneg a : α) = max a 0 :=
  rfl
Canonical Map to Nonnegative Elements Yields Maximum with Zero
Informal description
For any element $a$ of type $\alpha$, the underlying value of the nonnegative element obtained by applying the canonical map `toNonneg` to $a$ is equal to the maximum of $a$ and $0$, i.e., $(toNonneg\, a : \alpha) = \max(a, 0)$.
Nonneg.toNonneg_of_nonneg theorem
{a : α} (h : 0 ≤ a) : toNonneg a = ⟨a, h⟩
Full source 
@[simp]
theorem toNonneg_of_nonneg {a : α} (h : 0 ≤ a) : toNonneg a = ⟨a, h⟩ := by simp [toNonneg, h]
Canonical Map Preserves Nonnegative Elements
Informal description
For any element $a$ of type $\alpha$ with a proof $h$ that $0 \leq a$, the canonical map to nonnegative elements sends $a$ to the pair $\langle a, h \rangle$.
Nonneg.toNonneg_coe theorem
{a : { x : α // 0 ≤ x }} : toNonneg (a : α) = a
Full source 
@[simp]
theorem toNonneg_coe {a : { x : α // 0 ≤ x }} : toNonneg (a : α) = a :=
  toNonneg_of_nonneg a.2
Canonical Map Fixes Nonnegative Elements
Informal description
For any nonnegative element $a \in \{x : \alpha \mid 0 \leq x\}$, the canonical map to nonnegative elements applied to the underlying value of $a$ returns $a$ itself, i.e., $\text{toNonneg}(a) = a$.
Nonneg.toNonneg_le theorem
{a : α} {b : { x : α // 0 ≤ x }} : toNonneg a ≤ b ↔ a ≤ b
Full source 
@[simp]
theorem toNonneg_le {a : α} {b : { x : α // 0 ≤ x }} : toNonnegtoNonneg a ≤ b ↔ a ≤ b := by
  obtain ⟨b, hb⟩ := b
  simp [toNonneg, hb]
Inequality Preservation in Canonical Nonnegative Map: $\text{toNonneg}(a) \leq b \leftrightarrow a \leq b$
Informal description
For any element $a$ of type $\alpha$ and any nonnegative element $b \in \{x : \alpha \mid 0 \leq x\}$, the canonical nonnegative image of $a$ is less than or equal to $b$ if and only if $a$ is less than or equal to $b$ in $\alpha$.
Nonneg.sub instance
[Sub α] : Sub { x : α // 0 ≤ x }
Full source 
instance sub [Sub α] : Sub { x : α // 0 ≤ x } :=
  ⟨fun x y => toNonneg (x - y)⟩
Subtraction on Nonnegative Elements
Informal description
For any type $\alpha$ with a subtraction operation, the subtype of nonnegative elements $\{x : \alpha \mid 0 \leq x\}$ inherits a subtraction operation.
Nonneg.mk_sub_mk theorem
[Sub α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) - ⟨y, hy⟩ = toNonneg (x - y)
Full source 
@[simp]
theorem mk_sub_mk [Sub α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    (⟨x, hx⟩ : { x : α // 0 ≤ x }) - ⟨y, hy⟩ = toNonneg (x - y) :=
  rfl
Subtraction of Nonnegative Elements Equals Canonical Nonnegative Image
Informal description
Let $\alpha$ be a type equipped with a subtraction operation, and let $x, y \in \alpha$ be nonnegative elements (i.e., $0 \leq x$ and $0 \leq y$). Then the subtraction of the nonnegative elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ is equal to the canonical nonnegative image of $x - y$ in $\alpha$, i.e., \[ \langle x, hx \rangle - \langle y, hy \rangle = \text{toNonneg}(x - y). \]
Nonneg.toNonneg_lt theorem
{a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b
Full source 
@[simp]
theorem toNonneg_lt {a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b := by
  obtain ⟨a, ha⟩ := a
  simp [toNonneg, ha.not_lt]
Strict Inequality Between Nonnegative Element and Canonical Nonnegative Image
Informal description
For any nonnegative element $a$ in the subtype $\{x : \alpha \mid 0 \leq x\}$ and any element $b$ of type $\alpha$, the strict inequality $a < \text{toNonneg}(b)$ holds if and only if the underlying element $\uparrow a$ is strictly less than $b$ in $\alpha$.