Nonneg.coe_zero
theorem Nonneg.coe_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α], ↑0 = 0
This theorem, `Nonneg.coe_zero`, states that for any type `α` that has a zero element and a preorder (a binary relation describing an order on `α`), the coercion of the numeric zero `0` to `α` equals the zero element of `α`. This basically means that `0` maps to the zero element of any type `α` that has a zero and a defined order.
More concisely: For any type with a zero element and a preorder, the coercion of the numeric zero equals the zero element under the preorder.
|
Nonneg.coe_one
theorem Nonneg.coe_one : ∀ {α : Type u_1} [inst : OrderedSemiring α], ↑1 = 1
The theorem `Nonneg.coe_one` states that for any type `α` which forms an ordered semiring, the coersion of the integer 1 (notated as `↑1`) is equal to the semiring's unity (notated as `1`). In other words, in any ordered semiring, the coersion of the integer 1 remains as 1.
More concisely: In an ordered semiring, the conversion of the integer 1 to the semiring's type is equal to the semiring's unity.
|
Nonneg.coe_add
theorem Nonneg.coe_add :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : { x // 0 ≤ x }),
↑(a + b) = ↑a + ↑b
This theorem, `Nonneg.coe_add`, states that for any type `α` that is an `AddZeroClass` (i.e., it supports addition and has a zero element), is a `Preorder` (i.e., it supports a less than or equal to relation that is transitive and reflexive), and is a `CovariantClass` (i.e., it supports a binary operation that preserves the relation), if `a` and `b` are non-negative instances of this type (denoted by `{ x // 0 ≤ x }`), then the operation of adding `a` and `b` and then applying the coercion to `α` (denoted by `↑(a + b)`) is the same as adding the results of coercing `a` and `b` to `α` individually and then adding those results (denoted by `↑a + ↑b`). In simpler terms, for non-negative numbers `a` and `b` in such a type, coercion and addition commute with each other.
More concisely: For any `AddZeroClass` and `Preorder` type `α` that is a `CovariantClass`, if `a` and `b` are non-negative instances of `α`, then `↑(a + b) = ↑a + ↑b`.
|