Documentation

Mathlib.Algebra.Order.Nonneg.Floor

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 #

instance Nonneg.archimedean {α : Type u_1} [OrderedAddCommMonoid α] [Archimedean α] :
Archimedean { x // 0 x }
theorem Nonneg.nat_floor_coe {α : Type u_1} [OrderedSemiring α] [FloorSemiring α] (a : { r // 0 r }) :
theorem Nonneg.nat_ceil_coe {α : Type u_1} [OrderedSemiring α] [FloorSemiring α] (a : { r // 0 r }) :