Mathlib.Algebra.Order.Nonneg.Floor

Module docstring

{"# 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. "}

Nonneg.floorSemiring instance

[Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] : FloorSemiring { r : α // 0 ≤ r }

Full source

instance floorSemiring [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] :
    FloorSemiring { r : α // 0 ≤ r } where
  floor a := ⌊(a : α)⌋₊
  ceil a := ⌈(a : α)⌉₊
  floor_of_neg ha := FloorSemiring.floor_of_neg ha
  gc_floor ha := FloorSemiring.gc_floor (Subtype.coe_le_coe.2 ha)
  gc_ceil a n := FloorSemiring.gc_ceil (a : α) n

Floor Semiring Structure on Nonnegative Elements

Informal description

For any ordered semiring $\alpha$ with a floor semiring structure, the subtype $\{r \in \alpha \mid 0 \leq r\}$ of nonnegative elements inherits a floor semiring structure from $\alpha$.

Nonneg.nat_floor_coe theorem

 [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) : ⌊(a : α)⌋₊ = ⌊a⌋₊

Full source

@[norm_cast]
theorem nat_floor_coe [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α]
    (a : { r : α // 0 ≤ r }) :
    ⌊(a : α)⌋₊ = ⌊a⌋₊ :=
  rfl

Natural Floor Function Preserved in Nonnegative Subtype

Informal description

For any ordered semiring $\alpha$ with a floor semiring structure and any nonnegative element $a \in \{r \in \alpha \mid 0 \leq r\}$, the natural floor of $a$ (viewed as an element of $\alpha$) is equal to the natural floor of $a$ in the subtype of nonnegative elements. That is, $\lfloor a \rfloor_\mathbb{N} = \lfloor a \rfloor_\mathbb{N}$ where the left-hand side is computed in $\alpha$ and the right-hand side is computed in the subtype.

Nonneg.nat_ceil_coe theorem

 [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α] (a : { r : α // 0 ≤ r }) : ⌈(a : α)⌉₊ = ⌈a⌉₊

Full source

@[norm_cast]
theorem nat_ceil_coe [Semiring α] [PartialOrder α] [IsOrderedRing α] [FloorSemiring α]
    (a : { r : α // 0 ≤ r }) :
    ⌈(a : α)⌉₊ = ⌈a⌉₊ :=
  rfl

Natural Ceiling Function Preserved in Nonnegative Subtype

Informal description

Let $\alpha$ be an ordered semiring with a floor semiring structure. For any nonnegative element $a \in \{r \in \alpha \mid 0 \leq r\}$, the natural ceiling of $a$ (viewed as an element of $\alpha$) is equal to the natural ceiling of $a$ in the subtype of nonnegative elements. That is, $\lceil a \rceil_\mathbb{N} = \lceil a \rceil_\mathbb{N}$ where both sides are computed in their respective contexts.