mathlib docs: algebra.floor

@[class]

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

Type u_2

floor : α → ℤ
le_floor : ∀ (z : ℤ) (x : α), z ≤ floor_ring.floor x ↔ ↑z ≤ x

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

Instances

source

@[instance]

def int.floor_ring :

floor_ring ℤ

Equations

int.floor_ring = {floor := id ℤ, le_floor := int.floor_ring._proof_1}

source

def floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :

α → ℤ

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

Equations

floor = floor_ring.floor

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 : α} :

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} [decidable_linear_ordered_comm_ring α] [floor_ring α] {x y : α} :

⌊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

def fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :

α → α

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

Equations

fract r = r - ↑⌊r⌋

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 α] :

α → ℤ

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

Equations

⌈x⌉ = -⌊-x⌋

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 : α} :

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 : α} :

0 ≤ q → 0 ≤ ⌈q⌉

source

def nat_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :

α → ℕ

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

nat_ceil a = ⌈a⌉.to_nat

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₂ : α} :

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 : α} :

0 ≤ a → ↑(nat_ceil a) < a + 1

source

theorem lt_of_nat_ceil_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : ℕ} :

nat_ceil x < n → x < ↑n

source

theorem le_of_nat_ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {x : α} {n : ℕ} :

nat_ceil x ≤ n → x ≤ ↑n

mathlib documentation

algebra.floor

Floor and Ceil

Summary

Main Definitions

Notations

Tags

General documentation

Additional documentation

Library

mathlib documentation

algebra.​floor

Floor and Ceil

Summary

Main Definitions

Notations

Tags

General documentation

Additional documentation

Library

algebra.floor