Nonnegative elements are archimedean #
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 α.
This is used to derive algebraic structures on ℝ≥0 and ℚ≥0 automatically.
Main declarations #
{x : α // 0 ≤ x}is afloor_semiringifαis.
@[protected, instance]
def
nonneg.archimedean
{α : Type u_1}
[ordered_add_comm_monoid α]
[archimedean α] :
archimedean {x // 0 ≤ x}
@[protected, instance]
def
nonneg.floor_semiring
{α : Type u_1}
[ordered_semiring α]
[floor_semiring α] :
floor_semiring {r // 0 ≤ r}
@[norm_cast]
theorem
nonneg.nat_floor_coe
{α : Type u_1}
[ordered_semiring α]
[floor_semiring α]
(a : {r // 0 ≤ r}) :
@[norm_cast]
theorem
nonneg.nat_ceil_coe
{α : Type u_1}
[ordered_semiring α]
[floor_semiring α]
(a : {r // 0 ≤ r}) :