Nonnegative elements are archimedean

This file defines instances and prove some properties about the nonnegative elements Nonneg α of an arbitrary type α.

This is used to derive algebraic structures on ℝ≥0 and ℚ≥0 automatically.

Main declarations

• Nonneg α is a FloorSemiring if α is.

@[instance_reducible]

instance Nonneg.floorSemiring {α : Type u_1} [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] : FloorSemiring (Nonneg α)

Equations

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

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

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