mathlib documentation

algebra.floor

Floor and ceil #

Summary #

We define floor, ceil, nat_floorand nat_ceil functions on linear ordered rings.

Main Definitions #

Notations #

Tags #

rounding, floor, ceil

Floor rings #

@[class]
structure floor_ring (α : Type u_2) [linear_ordered_ring α] :
Type u_2

A floor_ring is a linear ordered ring over α with a function floor : α → ℤ satisfying ∀ (z : ℤ) (x : α), z ≤ floor x ↔ (z : α) ≤ x).

Instances
@[instance]
Equations
def floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
α →

floor x is the greatest integer z such that z ≤ x

Equations
theorem le_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {x : α} :
theorem floor_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {z : } :
x < z x < z
theorem floor_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
theorem floor_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
0 x 0 x
theorem lt_succ_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
theorem lt_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
theorem sub_one_lt_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
@[simp]
theorem floor_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
@[simp]
theorem floor_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
@[simp]
theorem floor_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem floor_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a b) :
@[simp]
theorem floor_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ) :
theorem floor_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ) :
theorem abs_sub_lt_one_of_floor_eq_floor {α : Type u_1} [linear_ordered_comm_ring α] [floor_ring α] {x y : α} (h : x = y) :
abs (x - y) < 1
theorem floor_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r : α} {z : } :
r = z z r r < z + 1
theorem floor_ring_unique {α : Type u_1} [linear_ordered_ring α] (inst1 inst2 : floor_ring α) :
theorem floor_eq_on_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (x : α) (H : x set.Ico n (n + 1)) :
theorem floor_eq_on_Ico' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (x : α) (H : x set.Ico n (n + 1)) :
def fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
α

The fractional part fract r of r is just r - ⌊r⌋

Equations
@[simp]
theorem floor_add_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
@[simp]
theorem fract_add_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
theorem fract_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
theorem fract_lt_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
fract r < 1
@[simp]
theorem fract_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
fract 0 = 0
@[simp]
theorem fract_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
@[simp]
theorem fract_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
@[simp]
theorem floor_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
theorem fract_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r s : α} :
fract r = s 0 s s < 1 ∃ (z : ), r - s = z
theorem fract_eq_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r s : α} :
fract r = fract s ∃ (z : ), r - s = z
@[simp]
theorem fract_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
theorem fract_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r s : α) :
∃ (z : ), fract (r + s) - fract r - fract s = z
theorem fract_mul_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) (b : ) :
∃ (z : ), (fract r) * b - fract (r * b) = z
def ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :

ceil x is the smallest integer z such that x ≤ z

Equations
theorem ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {x : α} :
theorem lt_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {z : } :
z < x z < x
theorem ceil_le_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
theorem le_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
@[simp]
theorem ceil_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
theorem ceil_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a b) :
@[simp]
theorem ceil_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ) :
theorem ceil_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ) :
theorem ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
theorem ceil_pos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < a 0 < a
@[simp]
theorem ceil_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem ceil_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {q : α} (hq : 0 q) :
theorem ceil_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r : α} {z : } :
r = z z - 1 < r r z
theorem ceil_eq_on_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (x : α) (H : x set.Ioc (n - 1) n) :
theorem ceil_eq_on_Ioc' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (x : α) (H : x set.Ioc (n - 1) n) :

nat_floor and nat_ceil #

def nat_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :

nat_floor x is the greatest natural n that is less than x. It is equal to ⌊q⌋ when q ≥ 0, and is 0 otherwise.

Equations
theorem nat_floor_of_nonpos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : a 0) :
theorem pos_of_nat_floor_pos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (h : 0 < nat_floor a) :
0 < a
theorem nat_floor_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 a) :
theorem le_nat_floor_of_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } (h : n a) :
theorem le_nat_floor_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } (ha : 0 a) :
theorem lt_of_lt_nat_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } (h : n < nat_floor a) :
n < a
theorem nat_floor_lt_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } (ha : 0 a) :
theorem nat_floor_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a₁ a₂ : α} (h : a₁ a₂) :
@[simp]
theorem nat_floor_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) :
@[simp]
theorem nat_floor_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem nat_floor_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 a) (n : ) :
theorem lt_nat_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
a < (nat_floor a) + 1
theorem nat_floor_eq_zero_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
nat_floor a = 0 a < 1
def nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :

nat_ceil x is the least natural n that is greater than x. It is equal to ⌈q⌉ when q ≥ 0, and is 0 otherwise.

Equations
theorem nat_ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } :
theorem lt_nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : } :
n < nat_ceil a n < a
theorem le_nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem nat_ceil_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a₁ a₂ : α} (h : a₁ a₂) :
@[simp]
theorem nat_ceil_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) :
@[simp]
theorem nat_ceil_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem nat_ceil_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (a_nonneg : 0 a) (n : ) :
theorem nat_ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (a_nonneg : 0 a) :
(nat_ceil a) < a + 1
theorem lt_of_nat_ceil_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : } (h : nat_ceil x < n) :
x < n
theorem le_of_nat_ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : } (h : nat_ceil x n) :
x n
@[simp]
theorem int.preimage_Ioo {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
@[simp]
theorem int.preimage_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
@[simp]
theorem int.preimage_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
@[simp]
theorem int.preimage_Icc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
@[simp]
theorem int.preimage_Ioi {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
@[simp]
theorem int.preimage_Ici {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
@[simp]
theorem int.preimage_Iio {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
@[simp]
theorem int.preimage_Iic {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :