mathlib3 documentation

algebra.order.floor

Floor and ceil #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings.

Main Definitions #

Notations #

The index ₊ in the notations for nat.floor and nat.ceil is used in analogy to the notation for nnnorm.

TODO #

linear_ordered_ring/linear_ordered_semiring can be relaxed to order_ring/order_semiring in many lemmas.

Tags #

rounding, floor, ceil

Floor semiring #

source
@[class]
structure floor_semiring (α : Type u_4) [ordered_semiring α] :
Type u_4

A floor_semiring is an ordered semiring over α with a function floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x). Note that many lemmas require a linear_order. Please see the above TODO.

Instances of this typeclass
Instances of other typeclasses for floor_semiring
  • floor_semiring.has_sizeof_inst
source
@[protected, instance]
def nat.floor_semiring  :
floor_semiring ℕ
Equations
source
def nat.floor {α : Type u_2} [ordered_semiring α] [floor_semiring α] :
α → ℕ

⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

Equations
source
def nat.ceil {α : Type u_2} [ordered_semiring α] [floor_semiring α] :
α → ℕ

⌈a⌉₊ is the least natural n such that a ≤ n

Equations
source
@[simp]
theorem nat.floor_nat  :
nat.floor = id
source
@[simp]
theorem nat.ceil_nat  :
nat.ceil = id
source
theorem nat.le_floor_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) :
n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
source
theorem nat.le_floor {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : ↑n ≤ a) :
n ≤ ⌊a⌋₊
source
theorem nat.floor_lt {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) :
⌊a⌋₊ < n ↔ a < ↑n
source
theorem nat.floor_lt_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
⌊a⌋₊ < 1 ↔ a < 1
source
theorem nat.lt_of_floor_lt {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : ⌊a⌋₊ < n) :
a < ↑n
source
theorem nat.lt_one_of_floor_lt_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (h : ⌊a⌋₊ < 1) :
a < 1
source
theorem nat.floor_le {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
↑⌊a⌋₊ ≤ a
source
theorem nat.lt_succ_floor {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
a < ↑(⌊a⌋₊.succ)
source
theorem nat.lt_floor_add_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
a < ↑⌊a⌋₊ + 1
source
@[simp]
theorem nat.floor_coe {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (n : ℕ) :
⌊↑n⌋₊ = n
source
@[simp]
theorem nat.floor_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
⌊0⌋₊ = 0
source
@[simp]
theorem nat.floor_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
⌊1⌋₊ = 1
source
theorem nat.floor_of_nonpos {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : a ≤ 0) :
⌊a⌋₊ = 0
source
theorem nat.floor_mono {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
monotone nat.floor
source
theorem nat.le_floor_iff' {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (hn : n ≠ 0) :
n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
source
@[simp]
theorem nat.one_le_floor_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (x : α) :
1 ≤ ⌊x⌋₊ ↔ 1 ≤ x
source
theorem nat.floor_lt' {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (hn : n ≠ 0) :
⌊a⌋₊ < n ↔ a < ↑n
source
theorem nat.floor_pos {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
0 < ⌊a⌋₊ ↔ 1 ≤ a
source
theorem nat.pos_of_floor_pos {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (h : 0 < ⌊a⌋₊) :
0 < a
source
theorem nat.lt_of_lt_floor {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : n < ⌊a⌋₊) :
↑n < a
source
theorem nat.floor_le_of_le {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : a ≤ ↑n) :
⌊a⌋₊ ≤ n
source
theorem nat.floor_le_one_of_le_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (h : a ≤ 1) :
⌊a⌋₊ ≤ 1
source
@[simp]
theorem nat.floor_eq_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
⌊a⌋₊ = 0 ↔ a < 1
source
theorem nat.floor_eq_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) :
⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
source
theorem nat.floor_eq_iff' {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (hn : n ≠ 0) :
⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
source
theorem nat.floor_eq_on_Ico {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (n : ℕ) (a : α) (H : a ∈ set.Ico ↑n (↑n + 1)) :
⌊a⌋₊ = n
source
theorem nat.floor_eq_on_Ico' {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (n : ℕ) (a : α) (H : a ∈ set.Ico ↑n (↑n + 1)) :
↑⌊a⌋₊ = ↑n
source
@[simp]
theorem nat.preimage_floor_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
nat.floor ⁻¹' {0} = set.Iio 1
source
theorem nat.preimage_floor_of_ne_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {n : ℕ} (hn : n ≠ 0) :
nat.floor ⁻¹' {n} = set.Ico ↑n (↑n + 1)

Ceil #

source
theorem nat.gc_ceil_coe {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
galois_connection nat.ceil coe
source
@[simp]
theorem nat.ceil_le {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} :
⌈a⌉₊ ≤ n ↔ a ≤ ↑n
source
theorem nat.lt_ceil {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} :
n < ⌈a⌉₊ ↔ ↑n < a
source
@[simp]
theorem nat.add_one_le_ceil_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} :
n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
source
@[simp]
theorem nat.one_le_ceil_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
1 ≤ ⌈a⌉₊ ↔ 0 < a
source
theorem nat.ceil_le_floor_add_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
⌈a⌉₊ ≤ ⌊a⌋₊ + 1
source
theorem nat.le_ceil {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
a ≤ ↑⌈a⌉₊
source
@[simp]
theorem nat.ceil_int_cast {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] (z : ℤ) :
⌈↑z⌉₊ = z.to_nat
source
@[simp]
theorem nat.ceil_nat_cast {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (n : ℕ) :
⌈↑n⌉₊ = n
source
theorem nat.ceil_mono {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
monotone nat.ceil
source
@[simp]
theorem nat.ceil_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
⌈0⌉₊ = 0
source
@[simp]
theorem nat.ceil_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
⌈1⌉₊ = 1
source
@[simp]
theorem nat.ceil_eq_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
⌈a⌉₊ = 0 ↔ a ≤ 0
source
@[simp]
theorem nat.ceil_pos {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
0 < ⌈a⌉₊ ↔ 0 < a
source
theorem nat.lt_of_ceil_lt {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : ⌈a⌉₊ < n) :
a < ↑n
source
theorem nat.le_of_ceil_le {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (h : ⌈a⌉₊ ≤ n) :
a ≤ ↑n
source
theorem nat.floor_le_ceil {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
⌊a⌋₊ ≤ ⌈a⌉₊
source
theorem nat.floor_lt_ceil_of_lt_of_pos {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a b : α} (h : a < b) (h' : 0 < b) :
⌊a⌋₊ < ⌈b⌉₊
source
theorem nat.ceil_eq_iff {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ} (hn : n ≠ 0) :
⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n
source
@[simp]
theorem nat.preimage_ceil_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] :
nat.ceil ⁻¹' {0} = set.Iic 0
source
theorem nat.preimage_ceil_of_ne_zero {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {n : ℕ} (hn : n ≠ 0) :
nat.ceil ⁻¹' {n} = set.Ioc ↑(n - 1) ↑n

Intervals #

source
@[simp]
theorem nat.preimage_Ioo {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a b : α} (ha : 0 ≤ a) :
coe ⁻¹' set.Ioo a b = set.Ioo ⌊a⌋₊ ⌈b⌉₊
source
@[simp]
theorem nat.preimage_Ico {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a b : α} :
coe ⁻¹' set.Ico a b = set.Ico ⌈a⌉₊ ⌈b⌉₊
source
@[simp]
theorem nat.preimage_Ioc {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
coe ⁻¹' set.Ioc a b = set.Ioc ⌊a⌋₊ ⌊b⌋₊
source
@[simp]
theorem nat.preimage_Icc {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a b : α} (hb : 0 ≤ b) :
coe ⁻¹' set.Icc a b = set.Icc ⌈a⌉₊ ⌊b⌋₊
source
@[simp]
theorem nat.preimage_Ioi {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
coe ⁻¹' set.Ioi a = set.Ioi ⌊a⌋₊
source
@[simp]
theorem nat.preimage_Ici {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
coe ⁻¹' set.Ici a = set.Ici ⌈a⌉₊
source
@[simp]
theorem nat.preimage_Iio {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
coe ⁻¹' set.Iio a = set.Iio ⌈a⌉₊
source
@[simp]
theorem nat.preimage_Iic {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
coe ⁻¹' set.Iic a = set.Iic ⌊a⌋₊
source
theorem nat.floor_add_nat {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) :
⌊a + ↑n⌋₊ = ⌊a⌋₊ + n
source
theorem nat.floor_add_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
⌊a + 1⌋₊ = ⌊a⌋₊ + 1
source
theorem nat.floor_sub_nat {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] [has_sub α] [has_ordered_sub α] [has_exists_add_of_le α] (a : α) (n : ℕ) :
⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
source
theorem nat.ceil_add_nat {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) :
⌈a + ↑n⌉₊ = ⌈a⌉₊ + n
source
theorem nat.ceil_add_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
⌈a + 1⌉₊ = ⌈a⌉₊ + 1
source
theorem nat.ceil_lt_add_one {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 ≤ a) :
↑⌈a⌉₊ < a + 1
source
theorem nat.ceil_add_le {α : Type u_2} [linear_ordered_semiring α] [floor_semiring α] (a b : α) :
⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
source
theorem nat.sub_one_lt_floor {α : Type u_2} [linear_ordered_ring α] [floor_semiring α] (a : α) :
a - 1 < ↑⌊a⌋₊
source
theorem nat.floor_div_nat {α : Type u_2} [linear_ordered_semifield α] [floor_semiring α] (a : α) (n : ℕ) :
⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
source
theorem nat.floor_div_eq_div {α : Type u_2} [linear_ordered_semifield α] [floor_semiring α] (m n : ℕ) :
⌊↑m / ↑n⌋₊ = m / n

Natural division is the floor of field division.

source
theorem subsingleton_floor_semiring {α : Type u_1} [linear_ordered_semiring α] :
subsingleton (floor_semiring α)

There exists at most one floor_semiring structure on a linear ordered semiring.

Floor rings #

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

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

Instances of this typeclass
Instances of other typeclasses for floor_ring
  • floor_ring.has_sizeof_inst
source
@[protected, instance]
def int.floor_ring  :
floor_ring ℤ
Equations
source
def floor_ring.of_floor (α : Type u_1) [linear_ordered_ring α] (floor : α → ℤ) (gc_coe_floor : galois_connection coe floor) :
floor_ring α

A floor_ring constructor from the floor function alone.

Equations
source
def floor_ring.of_ceil (α : Type u_1) [linear_ordered_ring α] (ceil : α → ℤ) (gc_ceil_coe : galois_connection ceil coe) :
floor_ring α

A floor_ring constructor from the ceil function alone.

Equations
source
def int.floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
α → ℤ

int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

Equations
source
def int.ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
α → ℤ

int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

Equations
source
def int.fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
α

int.fract a, the fractional part of a, is a minus its floor.

Equations
source
@[simp]
theorem int.floor_int  :
int.floor = id
source
@[simp]
theorem int.ceil_int  :
int.ceil = id
source
@[simp]
theorem int.fract_int  :
int.fract = 0
source
@[simp]
theorem int.floor_ring_floor_eq  :
floor_ring.floor = int.floor
source
@[simp]
theorem int.floor_ring_ceil_eq  :
floor_ring.ceil = int.ceil

Floor #

source
theorem int.gc_coe_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
galois_connection coe int.floor
source
theorem int.le_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
z ≤ ⌊a⌋ ↔ ↑z ≤ a
source
theorem int.floor_lt {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
⌊a⌋ < z ↔ a < ↑z
source
theorem int.floor_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
↑⌊a⌋ ≤ a
source
theorem int.floor_nonneg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 ≤ ⌊a⌋ ↔ 0 ≤ a
source
@[simp]
theorem int.floor_le_sub_one_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
⌊a⌋ ≤ z - 1 ↔ a < ↑z
source
@[simp]
theorem int.floor_le_neg_one_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
⌊a⌋ ≤ -1 ↔ a < 0
source
theorem int.floor_nonpos {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : a ≤ 0) :
⌊a⌋ ≤ 0
source
theorem int.lt_succ_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a < ↑(⌊a⌋.succ)
source
@[simp]
theorem int.lt_floor_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a < ↑⌊a⌋ + 1
source
@[simp]
theorem int.sub_one_lt_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a - 1 < ↑⌊a⌋
source
@[simp]
theorem int.floor_int_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
⌊↑z⌋ = z
source
@[simp]
theorem int.floor_nat_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) :
⌊↑n⌋ = ↑n
source
@[simp]
theorem int.floor_zero {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
⌊0⌋ = 0
source
@[simp]
theorem int.floor_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
⌊1⌋ = 1
source
theorem int.floor_mono {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
monotone int.floor
source
theorem int.floor_pos {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < ⌊a⌋ ↔ 1 ≤ a
source
@[simp]
theorem int.floor_add_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ℤ) :
⌊a + ↑z⌋ = ⌊a⌋ + z
source
theorem int.floor_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌊a + 1⌋ = ⌊a⌋ + 1
source
theorem int.le_floor_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
source
theorem int.le_floor_add_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋
source
@[simp]
theorem int.floor_int_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) (a : α) :
⌊↑z + a⌋ = z + ⌊a⌋
source
@[simp]
theorem int.floor_add_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ℕ) :
⌊a + ↑n⌋ = ⌊a⌋ + ↑n
source
@[simp]
theorem int.floor_nat_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) (a : α) :
⌊↑n + a⌋ = ↑n + ⌊a⌋
source
@[simp]
theorem int.floor_sub_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ℤ) :
⌊a - ↑z⌋ = ⌊a⌋ - z
source
@[simp]
theorem int.floor_sub_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ℕ) :
⌊a - ↑n⌋ = ⌊a⌋ - ↑n
source
theorem int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_1} [linear_ordered_comm_ring α] [floor_ring α] {a b : α} (h : ⌊a⌋ = ⌊b⌋) :
|a - b| < 1
source
theorem int.floor_eq_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
source
@[simp]
theorem int.floor_eq_zero_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
⌊a⌋ = 0 ↔ a ∈ set.Ico 0 1
source
theorem int.floor_eq_on_Ico {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (a : α) (H : a ∈ set.Ico ↑n (↑n + 1)) :
⌊a⌋ = n
source
theorem int.floor_eq_on_Ico' {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℤ) (a : α) (H : a ∈ set.Ico ↑n (↑n + 1)) :
↑⌊a⌋ = ↑n
source
@[simp]
theorem int.preimage_floor_singleton {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (m : ℤ) :
int.floor ⁻¹' {m} = set.Ico ↑m (↑m + 1)

Fractional part #

source
@[simp]
theorem int.self_sub_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a - ↑⌊a⌋ = int.fract a
source
@[simp]
theorem int.floor_add_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
↑⌊a⌋ + int.fract a = a
source
@[simp]
theorem int.fract_add_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract a + ↑⌊a⌋ = a
source
@[simp]
theorem int.fract_add_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (m : ℤ) :
int.fract (a + ↑m) = int.fract a
source
@[simp]
theorem int.fract_add_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (m : ℕ) :
int.fract (a + ↑m) = int.fract a
source
@[simp]
theorem int.fract_sub_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (m : ℤ) :
int.fract (a - ↑m) = int.fract a
source
@[simp]
theorem int.fract_int_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (m : ℤ) (a : α) :
int.fract (↑m + a) = int.fract a
source
@[simp]
theorem int.fract_sub_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ℕ) :
int.fract (a - ↑n) = int.fract a
source
@[simp]
theorem int.fract_int_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) (a : α) :
int.fract (↑n + a) = int.fract a
source
theorem int.fract_add_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
int.fract (a + b) ≤ int.fract a + int.fract b
source
theorem int.fract_add_fract_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
int.fract a + int.fract b ≤ int.fract (a + b) + 1
source
@[simp]
theorem int.self_sub_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a - int.fract a = ↑⌊a⌋
source
@[simp]
theorem int.fract_sub_self {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract a - a = -↑⌊a⌋
source
@[simp]
theorem int.fract_nonneg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
0 ≤ int.fract a
source
theorem int.fract_pos {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < int.fract a ↔ a ≠ ↑⌊a⌋

The fractional part of a is positive if and only if a ≠ ⌊a⌋.

source
theorem int.fract_lt_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract a < 1
source
@[simp]
theorem int.fract_zero {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
int.fract 0 = 0
source
@[simp]
theorem int.fract_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
int.fract 1 = 0
source
theorem int.abs_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
|int.fract a| = int.fract a
source
@[simp]
theorem int.abs_one_sub_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
|1 - int.fract a| = 1 - int.fract a
source
@[simp]
theorem int.fract_int_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
int.fract ↑z = 0
source
@[simp]
theorem int.fract_nat_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) :
int.fract ↑n = 0
source
@[simp]
theorem int.fract_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract ↑⌊a⌋ = 0
source
@[simp]
theorem int.floor_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌊int.fract a⌋ = 0
source
theorem int.fract_eq_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
int.fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = ↑z
source
theorem int.fract_eq_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
int.fract a = int.fract b ↔ ∃ (z : ℤ), a - b = ↑z
source
@[simp]
theorem int.fract_eq_self {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
int.fract a = a ↔ 0 ≤ a ∧ a < 1
source
@[simp]
theorem int.fract_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract (int.fract a) = int.fract a
source
theorem int.fract_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
∃ (z : ℤ), int.fract (a + b) - int.fract a - int.fract b = ↑z
source
theorem int.fract_neg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {x : α} (hx : int.fract x ≠ 0) :
int.fract (-x) = 1 - int.fract x
source
@[simp]
theorem int.fract_neg_eq_zero {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {x : α} :
int.fract (-x) = 0 ↔ int.fract x = 0
source
theorem int.fract_mul_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (b : ℕ) :
∃ (z : ℤ), int.fract a * ↑b - int.fract (a * ↑b) = ↑z
source
theorem int.preimage_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (s : set α) :
int.fract ⁻¹' s = ⋃ (m : ℤ), (λ (x : α), x - ↑m) ⁻¹' (s ∩ set.Ico 0 1)
source
theorem int.image_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (s : set α) :
int.fract '' s = ⋃ (m : ℤ), (λ (x : α), x - ↑m) '' s ∩ set.Ico 0 1
source
theorem int.fract_div_mul_self_mem_Ico {k : Type u_4} [linear_ordered_field k] [floor_ring k] (a b : k) (ha : 0 < a) :
int.fract (b / a) * a ∈ set.Ico 0 a
source
theorem int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [linear_ordered_field k] [floor_ring k] (a b : k) (ha : a ≠ 0) :
int.fract (b / a) * a + ⌊b / a⌋ • a = b
source
theorem int.sub_floor_div_mul_nonneg {k : Type u_4} [linear_ordered_field k] [floor_ring k] {b : k} (a : k) (hb : 0 < b) :
0 ≤ a - ↑⌊a / b⌋ * b
source
theorem int.sub_floor_div_mul_lt {k : Type u_4} [linear_ordered_field k] [floor_ring k] {b : k} (a : k) (hb : 0 < b) :
a - ↑⌊a / b⌋ * b < b
source
theorem int.fract_div_nat_cast_eq_div_nat_cast_mod {k : Type u_4} [linear_ordered_field k] [floor_ring k] {m n : ℕ} :
int.fract (↑m / ↑n) = ↑(m % n) / ↑n
source
theorem int.fract_div_int_cast_eq_div_int_cast_mod {k : Type u_4} [linear_ordered_field k] [floor_ring k] {m : ℤ} {n : ℕ} :
int.fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Ceil #

source
theorem int.gc_ceil_coe {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
galois_connection int.ceil coe
source
theorem int.ceil_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
⌈a⌉ ≤ z ↔ a ≤ ↑z
source
theorem int.floor_neg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
⌊-a⌋ = -⌈a⌉
source
theorem int.ceil_neg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
⌈-a⌉ = -⌊a⌋
source
theorem int.lt_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
z < ⌈a⌉ ↔ ↑z < a
source
@[simp]
theorem int.add_one_le_ceil_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
z + 1 ≤ ⌈a⌉ ↔ ↑z < a
source
@[simp]
theorem int.one_le_ceil_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
1 ≤ ⌈a⌉ ↔ 0 < a
source
theorem int.ceil_le_floor_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌈a⌉ ≤ ⌊a⌋ + 1
source
theorem int.le_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
a ≤ ↑⌈a⌉
source
@[simp]
theorem int.ceil_int_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) :
⌈↑z⌉ = z
source
@[simp]
theorem int.ceil_nat_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) :
⌈↑n⌉ = ↑n
source
theorem int.ceil_mono {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
monotone int.ceil
source
@[simp]
theorem int.ceil_add_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ℤ) :
⌈a + ↑z⌉ = ⌈a⌉ + z
source
@[simp]
theorem int.ceil_add_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ℕ) :
⌈a + ↑n⌉ = ⌈a⌉ + ↑n
source
@[simp]
theorem int.ceil_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌈a + 1⌉ = ⌈a⌉ + 1
source
@[simp]
theorem int.ceil_sub_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ℤ) :
⌈a - ↑z⌉ = ⌈a⌉ - z
source
@[simp]
theorem int.ceil_sub_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ℕ) :
⌈a - ↑n⌉ = ⌈a⌉ - ↑n
source
@[simp]
theorem int.ceil_sub_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌈a - 1⌉ = ⌈a⌉ - 1
source
theorem int.ceil_lt_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
↑⌈a⌉ < a + 1
source
theorem int.ceil_add_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
source
theorem int.ceil_add_ceil_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a b : α) :
⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1
source
@[simp]
theorem int.ceil_pos {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < ⌈a⌉ ↔ 0 < a
source
@[simp]
theorem int.ceil_zero {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
⌈0⌉ = 0
source
@[simp]
theorem int.ceil_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
⌈1⌉ = 1
source
theorem int.ceil_nonneg {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 ≤ a) :
0 ≤ ⌈a⌉
source
theorem int.ceil_eq_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α} :
⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
source
@[simp]
theorem int.ceil_eq_zero_iff {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
⌈a⌉ = 0 ↔ a ∈ set.Ioc (-1) 0
source
theorem int.ceil_eq_on_Ioc {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) (a : α) (H : a ∈ set.Ioc (↑z - 1) ↑z) :
⌈a⌉ = z
source
theorem int.ceil_eq_on_Ioc' {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (z : ℤ) (a : α) (H : a ∈ set.Ioc (↑z - 1) ↑z) :
↑⌈a⌉ = ↑z
source
theorem int.floor_le_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌊a⌋ ≤ ⌈a⌉
source
theorem int.floor_lt_ceil_of_lt {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a < b) :
⌊a⌋ < ⌈b⌉
source
@[simp]
theorem int.preimage_ceil_singleton {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (m : ℤ) :
int.ceil ⁻¹' {m} = set.Ioc (↑m - 1) ↑m
source
theorem int.fract_eq_zero_or_add_one_sub_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
int.fract a = 0 ∨ int.fract a = a + 1 - ↑⌈a⌉
source
theorem int.ceil_eq_add_one_sub_fract {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : int.fract a ≠ 0) :
↑⌈a⌉ = a + 1 - int.fract a
source
theorem int.ceil_sub_self_eq {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : int.fract a ≠ 0) :
↑⌈a⌉ - a = 1 - int.fract a

Intervals #

source
@[simp]
theorem int.preimage_Ioo {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
coe ⁻¹' set.Ioo a b = set.Ioo ⌊a⌋ ⌈b⌉
source
@[simp]
theorem int.preimage_Ico {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
coe ⁻¹' set.Ico a b = set.Ico ⌈a⌉ ⌈b⌉
source
@[simp]
theorem int.preimage_Ioc {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
coe ⁻¹' set.Ioc a b = set.Ioc ⌊a⌋ ⌊b⌋
source
@[simp]
theorem int.preimage_Icc {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a b : α} :
coe ⁻¹' set.Icc a b = set.Icc ⌈a⌉ ⌊b⌋
source
@[simp]
theorem int.preimage_Ioi {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
coe ⁻¹' set.Ioi a = set.Ioi ⌊a⌋
source
@[simp]
theorem int.preimage_Ici {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
coe ⁻¹' set.Ici a = set.Ici ⌈a⌉
source
@[simp]
theorem int.preimage_Iio {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
coe ⁻¹' set.Iio a = set.Iio ⌈a⌉
source
@[simp]
theorem int.preimage_Iic {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} :
coe ⁻¹' set.Iic a = set.Iic ⌊a⌋

Round #

source
def round {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) :
ℤ

round rounds a number to the nearest integer. round (1 / 2) = 1

Equations
source
@[simp]
theorem round_zero {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
round 0 = 0
source
@[simp]
theorem round_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
round 1 = 1
source
@[simp]
theorem round_nat_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℕ) :
round ↑n = ↑n
source
@[simp]
theorem round_int_cast {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (n : ℤ) :
round ↑n = n
source
@[simp]
theorem round_add_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℤ) :
round (x + ↑y) = round x + y
source
@[simp]
theorem round_add_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
round (a + 1) = round a + 1
source
@[simp]
theorem round_sub_int {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℤ) :
round (x - ↑y) = round x - y
source
@[simp]
theorem round_sub_one {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
round (a - 1) = round a - 1
source
@[simp]
theorem round_add_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℕ) :
round (x + ↑y) = round x + ↑y
source
@[simp]
theorem round_sub_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℕ) :
round (x - ↑y) = round x - ↑y
source
@[simp]
theorem round_int_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℤ) :
round (↑y + x) = y + round x
source
@[simp]
theorem round_nat_add {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (y : ℕ) :
round (↑y + x) = ↑y + round x
source
theorem abs_sub_round_eq_min {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) :
|x - ↑(round x)| = linear_order.min (int.fract x) (1 - int.fract x)
source
theorem round_le {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (x : α) (z : ℤ) :
|x - ↑(round x)| ≤ |x - ↑z|
source
theorem round_eq {α : Type u_2} [linear_ordered_field α] [floor_ring α] (x : α) :
round x = ⌊x + 1 / 2⌋
source
@[simp]
theorem round_two_inv {α : Type u_2} [linear_ordered_field α] [floor_ring α] :
round 2⁻¹ = 1
source
@[simp]
theorem round_neg_two_inv {α : Type u_2} [linear_ordered_field α] [floor_ring α] :
round (-2⁻¹) = 0
source
@[simp]
theorem round_eq_zero_iff {α : Type u_2} [linear_ordered_field α] [floor_ring α] {x : α} :
round x = 0 ↔ x ∈ set.Ico (-(1 / 2)) (1 / 2)
source
theorem abs_sub_round {α : Type u_2} [linear_ordered_field α] [floor_ring α] (x : α) :
|x - ↑(round x)| ≤ 1 / 2
source
theorem abs_sub_round_div_nat_cast_eq {α : Type u_2} [linear_ordered_field α] [floor_ring α] {m n : ℕ} :
|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(linear_order.min (m % n) (n - m % n)) / ↑n
source
theorem nat.floor_congr {α : Type u_2} {β : Type u_3} [linear_ordered_semiring α] [linear_ordered_semiring β] [floor_semiring α] [floor_semiring β] {a : α} {b : β} (h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b) :
⌊a⌋₊ = ⌊b⌋₊
source
theorem nat.ceil_congr {α : Type u_2} {β : Type u_3} [linear_ordered_semiring α] [linear_ordered_semiring β] [floor_semiring α] [floor_semiring β] {a : α} {b : β} (h : ∀ (n : ℕ), a ≤ ↑n ↔ b ≤ ↑n) :
⌈a⌉₊ = ⌈b⌉₊
source
theorem nat.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_semiring α] [linear_ordered_semiring β] [floor_semiring α] [floor_semiring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
⌊⇑f a⌋₊ = ⌊a⌋₊
source
theorem nat.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_semiring α] [linear_ordered_semiring β] [floor_semiring α] [floor_semiring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
⌈⇑f a⌉₊ = ⌈a⌉₊
source
theorem int.floor_congr {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_ring β] [floor_ring α] [floor_ring β] {a : α} {b : β} (h : ∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b) :
⌊a⌋ = ⌊b⌋
source
theorem int.ceil_congr {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_ring β] [floor_ring α] [floor_ring β] {a : α} {b : β} (h : ∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n) :
⌈a⌉ = ⌈b⌉
source
theorem int.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_ring β] [floor_ring α] [floor_ring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
⌊⇑f a⌋ = ⌊a⌋
source
theorem int.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_ring β] [floor_ring α] [floor_ring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
⌈⇑f a⌉ = ⌈a⌉
source
theorem int.map_fract {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_ring α] [linear_ordered_ring β] [floor_ring α] [floor_ring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
int.fract (⇑f a) = ⇑f (int.fract a)
source
theorem int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [linear_ordered_field β] [floor_ring α] [floor_ring β] [ring_hom_class F α β] (f : F) (hf : strict_mono ⇑f) (a : α) :
round (⇑f a) = round a

A floor ring as a floor semiring #

source
@[protected, instance]
def floor_ring.to_floor_semiring {α : Type u_2} [linear_ordered_ring α] [floor_ring α] :
floor_semiring α
Equations
source
theorem int.floor_to_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌊a⌋.to_nat = ⌊a⌋₊
source
theorem int.ceil_to_nat {α : Type u_2} [linear_ordered_ring α] [floor_ring α] (a : α) :
⌈a⌉.to_nat = ⌈a⌉₊
source
@[simp]
theorem nat.floor_int  :
nat.floor = int.to_nat
source
@[simp]
theorem nat.ceil_int  :
nat.ceil = int.to_nat
source
theorem nat.cast_floor_eq_int_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 ≤ a) :
↑⌊a⌋₊ = ⌊a⌋
source
theorem nat.cast_floor_eq_cast_int_floor {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 ≤ a) :
↑⌊a⌋₊ = ↑⌊a⌋
source
theorem nat.cast_ceil_eq_int_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 ≤ a) :
↑⌈a⌉₊ = ⌈a⌉
source
theorem nat.cast_ceil_eq_cast_int_ceil {α : Type u_2} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 ≤ a) :
↑⌈a⌉₊ = ↑⌈a⌉
source
theorem subsingleton_floor_ring {α : Type u_1} [linear_ordered_ring α] :
subsingleton (floor_ring α)

There exists at most one floor_ring structure on a given linear ordered ring.

source
meta def tactic.positivity_floor  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: int.floor is nonnegative if its input is.

source
meta def tactic.positivity_ceil  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: ceil and int.ceil are positive/nonnegative if their input is.