Nonnegative elements are archimedean

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 a FloorSemiring if α is.

instance Nonneg.floorSemiring {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] : FloorSemiring { r : α // 0 ≤ r }

Equations

• Nonneg.floorSemiring = { floor := fun (a : { r : α // 0 ≤ r }) => ⌊↑a⌋₊, ceil := fun (a : { r : α // 0 ≤ r }) => ⌈↑a⌉₊, floor_of_neg := ⋯, gc_floor := ⋯, gc_ceil := ⋯ }

theorem Nonneg.nat_floor_coe {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) : ⌊↑a⌋₊ = ⌊a⌋₊

theorem Nonneg.nat_ceil_coe {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) : ⌈↑a⌉₊ = ⌈a⌉₊