mathlib3 documentation

algebra.order.nonneg.ring

The type of nonnegative elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Main declarations #

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 and 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
@[protected, instance]
def nonneg.order_bot {α : Type u_1} [preorder α] {a : α} :
order_bot {x // a ≤ x}

This instance uses data fields from subtype.partial_order 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
source
theorem nonneg.bot_eq {α : Type u_1} [preorder α] {a : α} :
⊥ = ⟨a, _⟩
source
@[protected, instance]
def nonneg.no_max_order {α : Type u_1} [partial_order α] [no_max_order α] {a : α} :
no_max_order {x // a ≤ x}
source
@[protected, instance]
def nonneg.semilattice_sup {α : Type u_1} [semilattice_sup α] {a : α} :
semilattice_sup {x // a ≤ x}
Equations
source
@[protected, instance]
def nonneg.semilattice_inf {α : Type u_1} [semilattice_inf α] {a : α} :
semilattice_inf {x // a ≤ x}
Equations
source
@[protected, instance]
def nonneg.distrib_lattice {α : Type u_1} [distrib_lattice α] {a : α} :
distrib_lattice {x // a ≤ x}
Equations
source
@[protected, instance]
def nonneg.densely_ordered {α : Type u_1} [preorder α] [densely_ordered α] {a : α} :
densely_ordered {x // a ≤ x}
source
@[protected, reducible]
noncomputable def nonneg.conditionally_complete_linear_order {α : Type u_1} [conditionally_complete_linear_order α] {a : α} :
conditionally_complete_linear_order {x // a ≤ x}

If Sup ∅ ≤ a then {x : α // a ≤ x} is a conditionally_complete_linear_order.

Equations
source
@[protected, reducible]
noncomputable def nonneg.conditionally_complete_linear_order_bot {α : Type u_1} [conditionally_complete_linear_order α] {a : α} (h : has_Sup.Sup ∅ ≤ a) :
conditionally_complete_linear_order_bot {x // a ≤ x}

If Sup ∅ ≤ a then {x : α // a ≤ x} is a conditionally_complete_linear_order_bot.

This instance uses data fields from subtype.linear_order 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
source
@[protected, instance]
def nonneg.inhabited {α : Type u_1} [preorder α] {a : α} :
inhabited {x // a ≤ x}
Equations
source
@[protected, instance]
def nonneg.has_zero {α : Type u_1} [has_zero α] [preorder α] :
has_zero {x // 0 ≤ x}
Equations
source
@[protected, simp, norm_cast]
theorem nonneg.coe_zero {α : Type u_1} [has_zero α] [preorder α] :
↑0 = 0
source
@[simp]
theorem nonneg.mk_eq_zero {α : Type u_1} [has_zero α] [preorder α] {x : α} (hx : 0 ≤ x) :
⟨x, hx⟩ = 0 ↔ x = 0
source
@[protected, instance]
def nonneg.has_add {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] :
has_add {x // 0 ≤ x}
Equations
source
@[simp]
theorem nonneg.mk_add_mk {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, _⟩
source
@[protected, simp, norm_cast]
theorem nonneg.coe_add {α : Type u_1} [add_zero_class α] [preorder α] [covariant_class α α has_add.add has_le.le] (a b : {x // 0 ≤ x}) :
↑(a + b) = ↑a + ↑b
source
@[protected, instance]
def nonneg.has_nsmul {α : Type u_1} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] :
has_smul ℕ {x // 0 ≤ x}
Equations
source
@[simp]
theorem nonneg.nsmul_mk {α : Type u_1} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] (n : ℕ) {x : α} (hx : 0 ≤ x) :
n • ⟨x, hx⟩ = ⟨n • x, _⟩
source
@[protected, simp, norm_cast]
theorem nonneg.coe_nsmul {α : Type u_1} [add_monoid α] [preorder α] [covariant_class α α has_add.add has_le.le] (n : ℕ) (a : {x // 0 ≤ x}) :
↑(n • a) = n • ↑a
source
@[protected, instance]
def nonneg.ordered_add_comm_monoid {α : Type u_1} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.linear_ordered_add_comm_monoid {α : Type u_1} [linear_ordered_add_comm_monoid α] :
linear_ordered_add_comm_monoid {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.ordered_cancel_add_comm_monoid {α : Type u_1} [ordered_cancel_add_comm_monoid α] :
ordered_cancel_add_comm_monoid {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.linear_ordered_cancel_add_comm_monoid {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] :
linear_ordered_cancel_add_comm_monoid {x // 0 ≤ x}
Equations
source
def nonneg.coe_add_monoid_hom {α : Type u_1} [ordered_add_comm_monoid α] :
{x // 0 ≤ x} →+ α

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

Equations
source
@[norm_cast]
theorem nonneg.nsmul_coe {α : Type u_1} [ordered_add_comm_monoid α] (n : ℕ) (r : {x // 0 ≤ x}) :
↑(n • r) = n • ↑r
source
@[protected, instance]
def nonneg.has_one {α : Type u_1} [ordered_semiring α] :
has_one {x // 0 ≤ x}
Equations
source
@[protected, simp, norm_cast]
theorem nonneg.coe_one {α : Type u_1} [ordered_semiring α] :
↑1 = 1
source
@[simp]
theorem nonneg.mk_eq_one {α : Type u_1} [ordered_semiring α] {x : α} (hx : 0 ≤ x) :
⟨x, hx⟩ = 1 ↔ x = 1
source
@[protected, instance]
def nonneg.has_mul {α : Type u_1} [ordered_semiring α] :
has_mul {x // 0 ≤ x}
Equations
source
@[protected, simp, norm_cast]
theorem nonneg.coe_mul {α : Type u_1} [ordered_semiring α] (a b : {x // 0 ≤ x}) :
↑(a * b) = ↑a * ↑b
source
@[simp]
theorem nonneg.mk_mul_mk {α : Type u_1} [ordered_semiring α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, _⟩
source
@[protected, instance]
def nonneg.add_monoid_with_one {α : Type u_1} [ordered_semiring α] :
add_monoid_with_one {x // 0 ≤ x}
Equations
source
@[protected, simp, norm_cast]
theorem nonneg.coe_nat_cast {α : Type u_1} [ordered_semiring α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem nonneg.mk_nat_cast {α : Type u_1} [ordered_semiring α] (n : ℕ) :
⟨↑n, _⟩ = ↑n
source
@[protected, instance]
def nonneg.has_pow {α : Type u_1} [ordered_semiring α] :
has_pow {x // 0 ≤ x} ℕ
Equations
source
@[protected, simp, norm_cast]
theorem nonneg.coe_pow {α : Type u_1} [ordered_semiring α] (a : {x // 0 ≤ x}) (n : ℕ) :
↑(a ^ n) = ↑a ^ n
source
@[simp]
theorem nonneg.mk_pow {α : Type u_1} [ordered_semiring α] {x : α} (hx : 0 ≤ x) (n : ℕ) :
⟨x, hx⟩ ^ n = ⟨x ^ n, _⟩
source
@[protected, instance]
def nonneg.ordered_semiring {α : Type u_1} [ordered_semiring α] :
ordered_semiring {x // 0 ≤ x}
Equations
  • nonneg.ordered_semiring = function.injective.ordered_semiring coe nonneg.ordered_semiring._proof_3 nonneg.ordered_semiring._proof_4 nonneg.ordered_semiring._proof_5 nonneg.ordered_semiring._proof_6 nonneg.ordered_semiring._proof_7 nonneg.ordered_semiring._proof_8 nonneg.ordered_semiring._proof_9 nonneg.ordered_semiring._proof_10
source
@[protected, instance]
def nonneg.strict_ordered_semiring {α : Type u_1} [strict_ordered_semiring α] :
strict_ordered_semiring {x // 0 ≤ x}
Equations
  • nonneg.strict_ordered_semiring = function.injective.strict_ordered_semiring coe nonneg.strict_ordered_semiring._proof_3 nonneg.strict_ordered_semiring._proof_4 nonneg.strict_ordered_semiring._proof_5 nonneg.strict_ordered_semiring._proof_6 nonneg.strict_ordered_semiring._proof_7 nonneg.strict_ordered_semiring._proof_8 nonneg.strict_ordered_semiring._proof_9 nonneg.strict_ordered_semiring._proof_10
source
@[protected, instance]
def nonneg.ordered_comm_semiring {α : Type u_1} [ordered_comm_semiring α] :
ordered_comm_semiring {x // 0 ≤ x}
Equations
  • nonneg.ordered_comm_semiring = function.injective.ordered_comm_semiring coe nonneg.ordered_comm_semiring._proof_3 nonneg.ordered_comm_semiring._proof_4 nonneg.ordered_comm_semiring._proof_5 nonneg.ordered_comm_semiring._proof_6 nonneg.ordered_comm_semiring._proof_7 nonneg.ordered_comm_semiring._proof_8 nonneg.ordered_comm_semiring._proof_9 nonneg.ordered_comm_semiring._proof_10
source
@[protected, instance]
def nonneg.strict_ordered_comm_semiring {α : Type u_1} [strict_ordered_comm_semiring α] :
strict_ordered_comm_semiring {x // 0 ≤ x}
Equations
  • nonneg.strict_ordered_comm_semiring = function.injective.strict_ordered_comm_semiring coe nonneg.strict_ordered_comm_semiring._proof_3 nonneg.strict_ordered_comm_semiring._proof_4 nonneg.strict_ordered_comm_semiring._proof_5 nonneg.strict_ordered_comm_semiring._proof_6 nonneg.strict_ordered_comm_semiring._proof_7 nonneg.strict_ordered_comm_semiring._proof_8 nonneg.strict_ordered_comm_semiring._proof_9 nonneg.strict_ordered_comm_semiring._proof_10
source
@[protected, instance]
def nonneg.monoid_with_zero {α : Type u_1} [ordered_semiring α] :
monoid_with_zero {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.comm_monoid_with_zero {α : Type u_1} [ordered_comm_semiring α] :
comm_monoid_with_zero {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.semiring {α : Type u_1} [ordered_semiring α] :
semiring {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.comm_semiring {α : Type u_1} [ordered_comm_semiring α] :
comm_semiring {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.nontrivial {α : Type u_1} [linear_ordered_semiring α] :
nontrivial {x // 0 ≤ x}
source
@[protected, instance]
def nonneg.linear_ordered_semiring {α : Type u_1} [linear_ordered_semiring α] :
linear_ordered_semiring {x // 0 ≤ x}
Equations
  • nonneg.linear_ordered_semiring = function.injective.linear_ordered_semiring coe nonneg.linear_ordered_semiring._proof_3 nonneg.linear_ordered_semiring._proof_4 nonneg.linear_ordered_semiring._proof_5 nonneg.linear_ordered_semiring._proof_6 nonneg.linear_ordered_semiring._proof_7 nonneg.linear_ordered_semiring._proof_8 nonneg.linear_ordered_semiring._proof_9 nonneg.linear_ordered_semiring._proof_10 nonneg.linear_ordered_semiring._proof_11 nonneg.linear_ordered_semiring._proof_12
source
@[protected, instance]
def nonneg.linear_ordered_comm_monoid_with_zero {α : Type u_1} [linear_ordered_comm_ring α] :
linear_ordered_comm_monoid_with_zero {x // 0 ≤ x}
Equations
source
def nonneg.coe_ring_hom {α : Type u_1} [ordered_semiring α] :
{x // 0 ≤ x} →+* α

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

Equations
source
@[protected, instance]
def nonneg.canonically_ordered_add_monoid {α : Type u_1} [ordered_ring α] :
canonically_ordered_add_monoid {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.canonically_ordered_comm_semiring {α : Type u_1} [ordered_comm_ring α] [no_zero_divisors α] :
canonically_ordered_comm_semiring {x // 0 ≤ x}
Equations
source
@[protected, instance]
def nonneg.canonically_linear_ordered_add_monoid {α : Type u_1} [linear_ordered_ring α] :
canonically_linear_ordered_add_monoid {x // 0 ≤ x}
Equations
source
def nonneg.to_nonneg {α : Type u_1} [has_zero α] [linear_order α] (a : α) :
{x // 0 ≤ x}

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

Equations
source
@[simp]
theorem nonneg.coe_to_nonneg {α : Type u_1} [has_zero α] [linear_order α] {a : α} :
↑(nonneg.to_nonneg a) = linear_order.max a 0
source
@[simp]
theorem nonneg.to_nonneg_of_nonneg {α : Type u_1} [has_zero α] [linear_order α] {a : α} (h : 0 ≤ a) :
nonneg.to_nonneg a = ⟨a, h⟩
source
@[simp]
theorem nonneg.to_nonneg_coe {α : Type u_1} [has_zero α] [linear_order α] {a : {x // 0 ≤ x}} :
nonneg.to_nonneg ↑a = a
source
@[simp]
theorem nonneg.to_nonneg_le {α : Type u_1} [has_zero α] [linear_order α] {a : α} {b : {x // 0 ≤ x}} :
nonneg.to_nonneg a ≤ b ↔ a ≤ ↑b
source
@[simp]
theorem nonneg.to_nonneg_lt {α : Type u_1} [has_zero α] [linear_order α] {a : {x // 0 ≤ x}} {b : α} :
a < nonneg.to_nonneg b ↔ ↑a < b
source
@[protected, instance]
def nonneg.has_sub {α : Type u_1} [has_zero α] [linear_order α] [has_sub α] :
has_sub {x // 0 ≤ x}
Equations
source
@[simp]
theorem nonneg.mk_sub_mk {α : Type u_1} [has_zero α] [linear_order α] [has_sub α] {x y : α} (hx : 0 ≤ x) (hy : 0 ≤ y) :
⟨x, hx⟩ - ⟨y, hy⟩ = nonneg.to_nonneg (x - y)
source
@[protected, instance]
def nonneg.has_ordered_sub {α : Type u_1} [linear_ordered_ring α] :
has_ordered_sub {x // 0 ≤ x}