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.archimedean {α : Type u_1} [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x // 0 ≤ x }

Equations

• @Nonneg.archimedean = @Nonneg.archimedean.proof_1

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

Equations

• One or more equations did not get rendered due to their size.

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

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