mathlib documentation

algebra.floor

Floor and Ceil #

Summary #

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

Main Definitions #

Notations #

Tags #

rounding

source
@[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
source
@[protected, instance]
def int.floor_ring  :
floor_ring ℤ
Equations
source
def floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
α → ℤ

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

Equations
source
theorem le_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {x : α} :
z ≤ ⌊x⌋ ↔ ↑z ≤ x
source
theorem floor_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {z : ℤ} :
⌊x⌋ < z ↔ x < ↑z
source
theorem floor_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
↑⌊x⌋ ≤ x
source
theorem floor_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
0 ≤ ⌊x⌋ ↔ 0 ≤ x
source
theorem lt_succ_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
x < ↑(⌊x⌋.succ)
source
theorem lt_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
x < ↑⌊x⌋ + 1
source
theorem sub_one_lt_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
x - 1 < ↑⌊x⌋
source
@[simp]
theorem floor_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
⌊↑z⌋ = z
source
@[simp]
theorem floor_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
⌊0⌋ = 0
source
@[simp]
theorem floor_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
⌊1⌋ = 1
source
theorem floor_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a ≤ b) :
⌊a⌋ ≤ ⌊b⌋
source
@[simp]
theorem floor_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ℤ) :
⌊x + ↑z⌋ = ⌊x⌋ + z
source
theorem floor_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ℤ) :
⌊x - ↑z⌋ = ⌊x⌋ - z
source
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
source
theorem floor_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r : α} {z : ℤ} :
⌊r⌋ = z ↔ ↑z ≤ r ∧ r < ↑z + 1
source
theorem floor_ring_unique {α : Type u_1} [linear_ordered_ring α] (inst1 inst2 : floor_ring α) :
floor = floor
source
theorem floor_eq_on_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (x : α) (H : x ∈ set.Ico ↑n (↑n + 1)) :
⌊x⌋ = n
source
theorem floor_eq_on_Ico' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (x : α) (H : x ∈ set.Ico ↑n (↑n + 1)) :
↑⌊x⌋ = ↑n
source
def fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
α

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

Equations
source
@[simp]
theorem floor_add_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
↑⌊r⌋ + fract r = r
source
@[simp]
theorem fract_add_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
fract r + ↑⌊r⌋ = r
source
theorem fract_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
0 ≤ fract r
source
theorem fract_lt_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
fract r < 1
source
@[simp]
theorem fract_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
fract 0 = 0
source
@[simp]
theorem fract_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
fract ↑z = 0
source
@[simp]
theorem fract_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
fract ↑⌊r⌋ = 0
source
@[simp]
theorem floor_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
⌊fract r⌋ = 0
source
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
source
theorem fract_eq_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r s : α} :
fract r = fract s ↔ ∃ (z : ℤ), r - s = ↑z
source
@[simp]
theorem fract_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) :
fract (fract r) = fract r
source
theorem fract_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r s : α) :
∃ (z : ℤ), fract (r + s) - fract r - fract s = ↑z
source
theorem fract_mul_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (r : α) (b : ℕ) :
∃ (z : ℤ), (fract r) * ↑b - fract (r * ↑b) = ↑z
source
def ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
ℤ

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

Equations
source
theorem ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {x : α} :
⌈x⌉ ≤ z ↔ x ≤ ↑z
source
theorem lt_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {z : ℤ} :
z < ⌈x⌉ ↔ ↑z < x
source
theorem ceil_le_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
⌈x⌉ ≤ ⌊x⌋ + 1
source
theorem le_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
x ≤ ↑⌈x⌉
source
@[simp]
theorem ceil_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
⌈↑z⌉ = z
source
theorem ceil_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a ≤ b) :
⌈a⌉ ≤ ⌈b⌉
source
@[simp]
theorem ceil_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ℤ) :
⌈x + ↑z⌉ = ⌈x⌉ + z
source
theorem ceil_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ℤ) :
⌈x - ↑z⌉ = ⌈x⌉ - z
source
theorem ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (x : α) :
↑⌈x⌉ < x + 1
source
theorem ceil_pos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < ⌈a⌉ ↔ 0 < a
source
@[simp]
theorem ceil_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
⌈0⌉ = 0
source
theorem ceil_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {q : α} (hq : 0 ≤ q) :
0 ≤ ⌈q⌉
source
theorem ceil_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {r : α} {z : ℤ} :
⌈r⌉ = z ↔ ↑z - 1 < r ∧ r ≤ ↑z
source
theorem ceil_eq_on_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (x : α) (H : x ∈ set.Ioc (↑n - 1) ↑n) :
⌈x⌉ = n
source
theorem ceil_eq_on_Ioc' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (x : α) (H : x ∈ set.Ioc (↑n - 1) ↑n) :
↑⌈x⌉ = ↑n
source
def nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
ℕ

nat_ceil x is the smallest nonnegative integer n with x ≤ n. It is the same as ⌈q⌉ when q ≥ 0, otherwise it is 0.

Equations
source
theorem nat_ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : ℕ} :
nat_ceil a ≤ n ↔ a ≤ ↑n
source
theorem lt_nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} {n : ℕ} :
n < nat_ceil a ↔ ↑n < a
source
theorem le_nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
a ≤ ↑(nat_ceil a)
source
theorem nat_ceil_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a₁ a₂ : α} (h : a₁ ≤ a₂) :
nat_ceil a₁ ≤ nat_ceil a₂
source
@[simp]
theorem nat_ceil_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ℕ) :
nat_ceil ↑n = n
source
@[simp]
theorem nat_ceil_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
nat_ceil 0 = 0
source
theorem nat_ceil_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (a_nonneg : 0 ≤ a) (n : ℕ) :
nat_ceil (a + ↑n) = nat_ceil a + n
source
theorem nat_ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (a_nonneg : 0 ≤ a) :
↑(nat_ceil a) < a + 1
source
theorem lt_of_nat_ceil_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : ℕ} (h : nat_ceil x < n) :
x < ↑n
source
theorem le_of_nat_ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : ℕ} (h : nat_ceil x ≤ n) :
x ≤ ↑n
source
@[simp]
theorem int.preimage_Ioo {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
coe ⁻¹' set.Ioo x y = set.Ioo ⌊x⌋ ⌈y⌉
source
@[simp]
theorem int.preimage_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
coe ⁻¹' set.Ico x y = set.Ico ⌈x⌉ ⌈y⌉
source
@[simp]
theorem int.preimage_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
coe ⁻¹' set.Ioc x y = set.Ioc ⌊x⌋ ⌊y⌋
source
@[simp]
theorem int.preimage_Icc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x y : α} :
coe ⁻¹' set.Icc x y = set.Icc ⌈x⌉ ⌊y⌋
source
@[simp]
theorem int.preimage_Ioi {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
coe ⁻¹' set.Ioi x = set.Ioi ⌊x⌋
source
@[simp]
theorem int.preimage_Ici {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
coe ⁻¹' set.Ici x = set.Ici ⌈x⌉
source
@[simp]
theorem int.preimage_Iio {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
coe ⁻¹' set.Iio x = set.Iio ⌈x⌉
source
@[simp]
theorem int.preimage_Iic {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} :
coe ⁻¹' set.Iic x = set.Iic ⌊x⌋