# Floor and ceil #

## Summary #

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

## Main Definitions #

• FloorSemiring: An ordered semiring with natural-valued floor and ceil.

• Nat.floor a: Greatest natural n such that n ≤ a. Equal to 0 if a < 0.

• Nat.ceil a: Least natural n such that a ≤ n.

• FloorRing: A linearly ordered ring with integer-valued floor and ceil.

• Int.floor a: Greatest integer z such that z ≤ a.

• Int.ceil a: Least integer z such that a ≤ z.

• Int.fract a: Fractional part of a, defined as a - floor a.

• round a: Nearest integer to a. It rounds halves towards infinity.

## Notations #

• ⌊a⌋₊ is Nat.floor a.
• ⌈a⌉₊ is Nat.ceil a.
• ⌊a⌋ is Int.floor a.
• ⌈a⌉ is Int.ceil a.

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

## TODO #

LinearOrderedRing/LinearOrderedSemiring can be relaxed to OrderedRing/OrderedSemiring in many lemmas.

## Tags #

rounding, floor, ceil

### Floor semiring #

class FloorSemiring (α : Type u_4) [] :
Type u_4

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

• floor : α

FloorSemiring.floor a computes the greatest natural n such that (n : α) ≤ a.

• ceil : α

FloorSemiring.ceil a computes the least natural n such that a ≤ (n : α).

• floor_of_neg : ∀ {a : α}, a < 0

FloorSemiring.floor of a negative element is zero.

• gc_floor : ∀ {a : α} {n : }, 0 a( n a)

A natural number n is smaller than FloorSemiring.floor a iff its coercion to α is smaller than a.

• gc_ceil : GaloisConnection FloorSemiring.ceil Nat.cast

FloorSemiring.ceil is the lower adjoint of the coercion ↑ : ℕ → α.

Instances
theorem FloorSemiring.floor_of_neg {α : Type u_4} [] [self : ] {a : α} (ha : a < 0) :

FloorSemiring.floor of a negative element is zero.

theorem FloorSemiring.gc_floor {α : Type u_4} [] [self : ] {a : α} {n : } (ha : 0 a) :
n a

A natural number n is smaller than FloorSemiring.floor a iff its coercion to α is smaller than a.

theorem FloorSemiring.gc_ceil {α : Type u_4} [] [self : ] :
GaloisConnection FloorSemiring.ceil Nat.cast

FloorSemiring.ceil is the lower adjoint of the coercion ↑ : ℕ → α.

Equations
def Nat.floor {α : Type u_2} [] [] :
α

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

Equations
• Nat.floor = FloorSemiring.floor
Instances For
def Nat.ceil {α : Type u_2} [] [] :
α

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

Equations
• Nat.ceil = FloorSemiring.ceil
Instances For
@[simp]
theorem Nat.floor_nat :
Nat.floor = id
@[simp]
theorem Nat.ceil_nat :
Nat.ceil = id

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Nat.le_floor_iff {α : Type u_2} [] {a : α} {n : } (ha : 0 a) :
n a⌋₊ n a
theorem Nat.le_floor {α : Type u_2} [] {a : α} {n : } (h : n a) :
theorem Nat.floor_lt {α : Type u_2} [] {a : α} {n : } (ha : 0 a) :
a⌋₊ < n a < n
theorem Nat.floor_lt_one {α : Type u_2} [] {a : α} (ha : 0 a) :
a⌋₊ < 1 a < 1
theorem Nat.lt_of_floor_lt {α : Type u_2} [] {a : α} {n : } (h : a⌋₊ < n) :
a < n
theorem Nat.lt_one_of_floor_lt_one {α : Type u_2} [] {a : α} (h : a⌋₊ < 1) :
a < 1
theorem Nat.floor_le {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem Nat.lt_succ_floor {α : Type u_2} [] (a : α) :
a < a⌋₊.succ
theorem Nat.lt_floor_add_one {α : Type u_2} [] (a : α) :
a < a⌋₊ + 1
@[simp]
theorem Nat.floor_natCast {α : Type u_2} [] (n : ) :
n⌋₊ = n
@[deprecated Nat.floor_natCast]
theorem Nat.floor_coe {α : Type u_2} [] (n : ) :
n⌋₊ = n

Alias of Nat.floor_natCast.

@[simp]
theorem Nat.floor_zero {α : Type u_2} [] :
@[simp]
theorem Nat.floor_one {α : Type u_2} [] :
@[simp]
theorem Nat.floor_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
theorem Nat.floor_of_nonpos {α : Type u_2} [] {a : α} (ha : a 0) :
theorem Nat.floor_mono {α : Type u_2} [] :
Monotone Nat.floor
theorem Nat.floor_le_floor {α : Type u_2} [] (x : α) (y : α) :
theorem Nat.le_floor_iff' {α : Type u_2} [] {a : α} {n : } (hn : n 0) :
n a⌋₊ n a
@[simp]
theorem Nat.one_le_floor_iff {α : Type u_2} [] (x : α) :
theorem Nat.floor_lt' {α : Type u_2} [] {a : α} {n : } (hn : n 0) :
a⌋₊ < n a < n
theorem Nat.floor_pos {α : Type u_2} [] {a : α} :
theorem Nat.pos_of_floor_pos {α : Type u_2} [] {a : α} (h : 0 < a⌋₊) :
0 < a
theorem Nat.lt_of_lt_floor {α : Type u_2} [] {a : α} {n : } (h : n < a⌋₊) :
n < a
theorem Nat.floor_le_of_le {α : Type u_2} [] {a : α} {n : } (h : a n) :
theorem Nat.floor_le_one_of_le_one {α : Type u_2} [] {a : α} (h : a 1) :
@[simp]
theorem Nat.floor_eq_zero {α : Type u_2} [] {a : α} :
a⌋₊ = 0 a < 1
theorem Nat.floor_eq_iff {α : Type u_2} [] {a : α} {n : } (ha : 0 a) :
a⌋₊ = n n a a < n + 1
theorem Nat.floor_eq_iff' {α : Type u_2} [] {a : α} {n : } (hn : n 0) :
a⌋₊ = n n a a < n + 1
theorem Nat.floor_eq_on_Ico {α : Type u_2} [] (n : ) (a : α) :
a Set.Ico (n) (n + 1)a⌋₊ = n
theorem Nat.floor_eq_on_Ico' {α : Type u_2} [] (n : ) (a : α) :
a Set.Ico (n) (n + 1)a⌋₊ = n
@[simp]
theorem Nat.preimage_floor_zero {α : Type u_2} [] :
Nat.floor ⁻¹' {0} =
theorem Nat.preimage_floor_of_ne_zero {α : Type u_2} [] {n : } (hn : n 0) :
Nat.floor ⁻¹' {n} = Set.Ico (n) (n + 1)

#### Ceil #

theorem Nat.gc_ceil_coe {α : Type u_2} [] :
GaloisConnection Nat.ceil Nat.cast
@[simp]
theorem Nat.ceil_le {α : Type u_2} [] {a : α} {n : } :
a⌉₊ n a n
theorem Nat.lt_ceil {α : Type u_2} [] {a : α} {n : } :
n < a⌉₊ n < a
theorem Nat.add_one_le_ceil_iff {α : Type u_2} [] {a : α} {n : } :
n + 1 a⌉₊ n < a
@[simp]
theorem Nat.one_le_ceil_iff {α : Type u_2} [] {a : α} :
theorem Nat.ceil_le_floor_add_one {α : Type u_2} [] (a : α) :
theorem Nat.le_ceil {α : Type u_2} [] (a : α) :
@[simp]
theorem Nat.ceil_intCast {α : Type u_4} [] (z : ) :
z⌉₊ = z.toNat
@[simp]
theorem Nat.ceil_natCast {α : Type u_2} [] (n : ) :
n⌉₊ = n
theorem Nat.ceil_mono {α : Type u_2} [] :
Monotone Nat.ceil
theorem Nat.ceil_le_ceil {α : Type u_2} [] (x : α) (y : α) :
@[simp]
theorem Nat.ceil_zero {α : Type u_2} [] :
@[simp]
theorem Nat.ceil_one {α : Type u_2} [] :
@[simp]
theorem Nat.ceil_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
@[simp]
theorem Nat.ceil_eq_zero {α : Type u_2} [] {a : α} :
@[simp]
theorem Nat.ceil_pos {α : Type u_2} [] {a : α} :
0 < a⌉₊ 0 < a
theorem Nat.lt_of_ceil_lt {α : Type u_2} [] {a : α} {n : } (h : a⌉₊ < n) :
a < n
theorem Nat.le_of_ceil_le {α : Type u_2} [] {a : α} {n : } (h : a⌉₊ n) :
a n
theorem Nat.floor_le_ceil {α : Type u_2} [] (a : α) :
theorem Nat.floor_lt_ceil_of_lt_of_pos {α : Type u_2} [] {a : α} {b : α} (h : a < b) (h' : 0 < b) :
theorem Nat.ceil_eq_iff {α : Type u_2} [] {a : α} {n : } (hn : n 0) :
a⌉₊ = n (n - 1) < a a n
@[simp]
theorem Nat.preimage_ceil_zero {α : Type u_2} [] :
Nat.ceil ⁻¹' {0} =
theorem Nat.preimage_ceil_of_ne_zero {α : Type u_2} [] {n : } (hn : n 0) :
Nat.ceil ⁻¹' {n} = Set.Ioc (n - 1) n

#### Intervals #

@[simp]
theorem Nat.preimage_Ioo {α : Type u_2} [] {a : α} {b : α} (ha : 0 a) :
Nat.cast ⁻¹' Set.Ioo a b =
@[simp]
theorem Nat.preimage_Ico {α : Type u_2} [] {a : α} {b : α} :
Nat.cast ⁻¹' Set.Ico a b =
@[simp]
theorem Nat.preimage_Ioc {α : Type u_2} [] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
Nat.cast ⁻¹' Set.Ioc a b =
@[simp]
theorem Nat.preimage_Icc {α : Type u_2} [] {a : α} {b : α} (hb : 0 b) :
Nat.cast ⁻¹' Set.Icc a b =
@[simp]
theorem Nat.preimage_Ioi {α : Type u_2} [] {a : α} (ha : 0 a) :
Nat.cast ⁻¹' =
@[simp]
theorem Nat.preimage_Ici {α : Type u_2} [] {a : α} :
Nat.cast ⁻¹' =
@[simp]
theorem Nat.preimage_Iio {α : Type u_2} [] {a : α} :
Nat.cast ⁻¹' =
@[simp]
theorem Nat.preimage_Iic {α : Type u_2} [] {a : α} (ha : 0 a) :
Nat.cast ⁻¹' =
theorem Nat.floor_add_nat {α : Type u_2} [] {a : α} (ha : 0 a) (n : ) :
theorem Nat.floor_add_one {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem Nat.floor_add_ofNat {α : Type u_2} [] {a : α} (ha : 0 a) (n : ) [n.AtLeastTwo] :
@[simp]
theorem Nat.floor_sub_nat {α : Type u_2} [] [Sub α] [] [] (a : α) (n : ) :
@[simp]
theorem Nat.floor_sub_one {α : Type u_2} [] [Sub α] [] [] (a : α) :
@[simp]
theorem Nat.floor_sub_ofNat {α : Type u_2} [] [Sub α] [] [] (a : α) (n : ) [n.AtLeastTwo] :
theorem Nat.ceil_add_nat {α : Type u_2} [] {a : α} (ha : 0 a) (n : ) :
theorem Nat.ceil_add_one {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem Nat.ceil_add_ofNat {α : Type u_2} [] {a : α} (ha : 0 a) (n : ) [n.AtLeastTwo] :
theorem Nat.ceil_lt_add_one {α : Type u_2} [] {a : α} (ha : 0 a) :
a⌉₊ < a + 1
theorem Nat.ceil_add_le {α : Type u_2} [] (a : α) (b : α) :
theorem Nat.sub_one_lt_floor {α : Type u_2} [] (a : α) :
a - 1 < a⌋₊
theorem Nat.floor_div_nat {α : Type u_2} [] (a : α) (n : ) :
theorem Nat.floor_div_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
theorem Nat.floor_div_eq_div {α : Type u_2} [] (m : ) (n : ) :
m / n⌋₊ = m / n

Natural division is the floor of field division.

theorem subsingleton_floorSemiring {α : Type u_4} :

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

### Floor rings #

class FloorRing (α : Type u_4) :
Type u_4

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

• floor : α

FloorRing.floor a computes the greatest integer z such that (z : α) ≤ a.

• ceil : α

FloorRing.ceil a computes the least integer z such that a ≤ (z : α).

• gc_coe_floor : GaloisConnection Int.cast FloorRing.floor

FloorRing.ceil is the upper adjoint of the coercion ↑ : ℤ → α.

• gc_ceil_coe : GaloisConnection FloorRing.ceil Int.cast

FloorRing.ceil is the lower adjoint of the coercion ↑ : ℤ → α.

Instances
theorem FloorRing.gc_coe_floor {α : Type u_4} [self : ] :
GaloisConnection Int.cast FloorRing.floor

FloorRing.ceil is the upper adjoint of the coercion ↑ : ℤ → α.

theorem FloorRing.gc_ceil_coe {α : Type u_4} [self : ] :
GaloisConnection FloorRing.ceil Int.cast

FloorRing.ceil is the lower adjoint of the coercion ↑ : ℤ → α.

instance instFloorRingInt :
Equations
def FloorRing.ofFloor (α : Type u_4) (floor : α) (gc_coe_floor : GaloisConnection Int.cast floor) :

A FloorRing constructor from the floor function alone.

Equations
• FloorRing.ofFloor α floor gc_coe_floor = { floor := floor, ceil := fun (a : α) => -floor (-a), gc_coe_floor := gc_coe_floor, gc_ceil_coe := }
Instances For
def FloorRing.ofCeil (α : Type u_4) (ceil : α) (gc_ceil_coe : GaloisConnection ceil Int.cast) :

A FloorRing constructor from the ceil function alone.

Equations
• FloorRing.ofCeil α ceil gc_ceil_coe = { floor := fun (a : α) => -ceil (-a), ceil := ceil, gc_coe_floor := , gc_ceil_coe := gc_ceil_coe }
Instances For
def Int.floor {α : Type u_2} [] :
α

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

Equations
• Int.floor = FloorRing.floor
Instances For
def Int.ceil {α : Type u_2} [] :
α

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

Equations
• Int.ceil = FloorRing.ceil
Instances For
def Int.fract {α : Type u_2} [] (a : α) :
α

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

Equations
Instances For
@[simp]
theorem Int.floor_int :
Int.floor = id
@[simp]
theorem Int.ceil_int :
Int.ceil = id
@[simp]
theorem Int.fract_int :
Int.fract = 0

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]

#### Floor #

theorem Int.gc_coe_floor {α : Type u_2} [] :
GaloisConnection Int.cast Int.floor
theorem Int.le_floor {α : Type u_2} [] {z : } {a : α} :
z a z a
theorem Int.floor_lt {α : Type u_2} [] {z : } {a : α} :
a < z a < z
theorem Int.floor_le {α : Type u_2} [] (a : α) :
a a
theorem Int.floor_nonneg {α : Type u_2} [] {a : α} :
0 a 0 a
@[simp]
theorem Int.floor_le_sub_one_iff {α : Type u_2} [] {z : } {a : α} :
a z - 1 a < z
@[simp]
theorem Int.floor_le_neg_one_iff {α : Type u_2} [] {a : α} :
a -1 a < 0
theorem Int.floor_nonpos {α : Type u_2} [] {a : α} (ha : a 0) :
theorem Int.lt_succ_floor {α : Type u_2} [] (a : α) :
a < a.succ
@[simp]
theorem Int.lt_floor_add_one {α : Type u_2} [] (a : α) :
a < a + 1
@[simp]
theorem Int.sub_one_lt_floor {α : Type u_2} [] (a : α) :
a - 1 < a
@[simp]
theorem Int.floor_intCast {α : Type u_2} [] (z : ) :
z = z
@[simp]
theorem Int.floor_natCast {α : Type u_2} [] (n : ) :
n = n
@[simp]
theorem Int.floor_zero {α : Type u_2} [] :
@[simp]
theorem Int.floor_one {α : Type u_2} [] :
@[simp]
theorem Int.floor_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
= n
theorem Int.floor_mono {α : Type u_2} [] :
Monotone Int.floor
theorem Int.floor_le_floor {α : Type u_2} [] (x : α) (y : α) :
x yx y
theorem Int.floor_pos {α : Type u_2} [] {a : α} :
0 < a 1 a
@[simp]
theorem Int.floor_add_int {α : Type u_2} [] (a : α) (z : ) :
a + z = a + z
@[simp]
theorem Int.floor_add_one {α : Type u_2} [] (a : α) :
a + 1 = a + 1
theorem Int.le_floor_add {α : Type u_2} [] (a : α) (b : α) :
theorem Int.le_floor_add_floor {α : Type u_2} [] (a : α) (b : α) :
@[simp]
theorem Int.floor_int_add {α : Type u_2} [] (z : ) (a : α) :
z + a = z + a
@[simp]
theorem Int.floor_add_nat {α : Type u_2} [] (a : α) (n : ) :
a + n = a + n
@[simp]
theorem Int.floor_add_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
@[simp]
theorem Int.floor_nat_add {α : Type u_2} [] (n : ) (a : α) :
n + a = n + a
@[simp]
theorem Int.floor_ofNat_add {α : Type u_2} [] (n : ) [n.AtLeastTwo] (a : α) :
@[simp]
theorem Int.floor_sub_int {α : Type u_2} [] (a : α) (z : ) :
a - z = a - z
@[simp]
theorem Int.floor_sub_nat {α : Type u_2} [] (a : α) (n : ) :
a - n = a - n
@[simp]
theorem Int.floor_sub_one {α : Type u_2} [] (a : α) :
a - 1 = a - 1
@[simp]
theorem Int.floor_sub_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
theorem Int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_4} [] {a : α} {b : α} (h : a = b) :
|a - b| < 1
theorem Int.floor_eq_iff {α : Type u_2} [] {z : } {a : α} :
a = z z a a < z + 1
@[simp]
theorem Int.floor_eq_zero_iff {α : Type u_2} [] {a : α} :
theorem Int.floor_eq_on_Ico {α : Type u_2} [] (n : ) (a : α) :
a Set.Ico (n) (n + 1)a = n
theorem Int.floor_eq_on_Ico' {α : Type u_2} [] (n : ) (a : α) :
a Set.Ico (n) (n + 1)a = n
@[simp]
theorem Int.preimage_floor_singleton {α : Type u_2} [] (m : ) :
Int.floor ⁻¹' {m} = Set.Ico (m) (m + 1)

#### Fractional part #

@[simp]
theorem Int.self_sub_floor {α : Type u_2} [] (a : α) :
a - a =
@[simp]
theorem Int.floor_add_fract {α : Type u_2} [] (a : α) :
a + = a
@[simp]
theorem Int.fract_add_floor {α : Type u_2} [] (a : α) :
+ a = a
@[simp]
theorem Int.fract_add_int {α : Type u_2} [] (a : α) (m : ) :
Int.fract (a + m) =
@[simp]
theorem Int.fract_add_nat {α : Type u_2} [] (a : α) (m : ) :
Int.fract (a + m) =
@[simp]
theorem Int.fract_add_one {α : Type u_2} [] (a : α) :
Int.fract (a + 1) =
@[simp]
theorem Int.fract_add_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
Int.fract (a + ) =
@[simp]
theorem Int.fract_int_add {α : Type u_2} [] (m : ) (a : α) :
Int.fract (m + a) =
@[simp]
theorem Int.fract_nat_add {α : Type u_2} [] (n : ) (a : α) :
Int.fract (n + a) =
@[simp]
theorem Int.fract_one_add {α : Type u_2} [] (a : α) :
Int.fract (1 + a) =
@[simp]
theorem Int.fract_ofNat_add {α : Type u_2} [] (n : ) [n.AtLeastTwo] (a : α) :
Int.fract ( + a) =
@[simp]
theorem Int.fract_sub_int {α : Type u_2} [] (a : α) (m : ) :
Int.fract (a - m) =
@[simp]
theorem Int.fract_sub_nat {α : Type u_2} [] (a : α) (n : ) :
Int.fract (a - n) =
@[simp]
theorem Int.fract_sub_one {α : Type u_2} [] (a : α) :
Int.fract (a - 1) =
@[simp]
theorem Int.fract_sub_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
Int.fract (a - ) =
theorem Int.fract_add_le {α : Type u_2} [] (a : α) (b : α) :
Int.fract (a + b)
theorem Int.fract_add_fract_le {α : Type u_2} [] (a : α) (b : α) :
Int.fract (a + b) + 1
@[simp]
theorem Int.self_sub_fract {α : Type u_2} [] (a : α) :
a - = a
@[simp]
theorem Int.fract_sub_self {α : Type u_2} [] (a : α) :
- a = -a
@[simp]
theorem Int.fract_nonneg {α : Type u_2} [] (a : α) :
0
theorem Int.fract_pos {α : Type u_2} [] {a : α} :
0 < a a

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

theorem Int.fract_lt_one {α : Type u_2} [] (a : α) :
< 1
@[simp]
theorem Int.fract_zero {α : Type u_2} [] :
= 0
@[simp]
theorem Int.fract_one {α : Type u_2} [] :
= 0
theorem Int.abs_fract {α : Type u_2} [] {a : α} :
|| =
@[simp]
theorem Int.abs_one_sub_fract {α : Type u_2} [] {a : α} :
|1 - | = 1 -
@[simp]
theorem Int.fract_intCast {α : Type u_2} [] (z : ) :
= 0
@[simp]
theorem Int.fract_natCast {α : Type u_2} [] (n : ) :
= 0
@[simp]
theorem Int.fract_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
= 0
theorem Int.fract_floor {α : Type u_2} [] (a : α) :
= 0
@[simp]
theorem Int.floor_fract {α : Type u_2} [] (a : α) :
= 0
theorem Int.fract_eq_iff {α : Type u_2} [] {a : α} {b : α} :
= b 0 b b < 1 ∃ (z : ), a - b = z
theorem Int.fract_eq_fract {α : Type u_2} [] {a : α} {b : α} :
∃ (z : ), a - b = z
@[simp]
theorem Int.fract_eq_self {α : Type u_2} [] {a : α} :
= a 0 a a < 1
@[simp]
theorem Int.fract_fract {α : Type u_2} [] (a : α) :
=
theorem Int.fract_add {α : Type u_2} [] (a : α) (b : α) :
∃ (z : ), Int.fract (a + b) - - = z
theorem Int.fract_neg {α : Type u_2} [] {x : α} (hx : 0) :
Int.fract (-x) = 1 -
@[simp]
theorem Int.fract_neg_eq_zero {α : Type u_2} [] {x : α} :
Int.fract (-x) = 0 = 0
theorem Int.fract_mul_nat {α : Type u_2} [] (a : α) (b : ) :
∃ (z : ), * b - Int.fract (a * b) = z
theorem Int.preimage_fract {α : Type u_2} [] (s : Set α) :
Int.fract ⁻¹' s = ⋃ (m : ), (fun (x : α) => x - m) ⁻¹' (s Set.Ico 0 1)
theorem Int.image_fract {α : Type u_2} [] (s : Set α) :
Int.fract '' s = ⋃ (m : ), (fun (x : α) => x - m) '' s Set.Ico 0 1
theorem Int.fract_div_mul_self_mem_Ico {k : Type u_4} [] (a : k) (b : k) (ha : 0 < a) :
Int.fract (b / a) * a Set.Ico 0 a
theorem Int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [] (a : k) (b : k) (ha : a 0) :
Int.fract (b / a) * a + b / a a = b
theorem Int.sub_floor_div_mul_nonneg {k : Type u_4} [] {b : k} (a : k) (hb : 0 < b) :
0 a - a / b * b
theorem Int.sub_floor_div_mul_lt {k : Type u_4} [] {b : k} (a : k) (hb : 0 < b) :
a - a / b * b < b
theorem Int.fract_div_natCast_eq_div_natCast_mod {k : Type u_4} [] {m : } {n : } :
Int.fract (m / n) = (m % n) / n
theorem Int.fract_div_intCast_eq_div_intCast_mod {k : Type u_4} [] {m : } {n : } :
Int.fract (m / n) = (m % n) / n

#### Ceil #

theorem Int.gc_ceil_coe {α : Type u_2} [] :
GaloisConnection Int.ceil Int.cast
theorem Int.ceil_le {α : Type u_2} [] {z : } {a : α} :
a z a z
theorem Int.floor_neg {α : Type u_2} [] {a : α} :
theorem Int.ceil_neg {α : Type u_2} [] {a : α} :
theorem Int.lt_ceil {α : Type u_2} [] {z : } {a : α} :
z < a z < a
@[simp]
theorem Int.add_one_le_ceil_iff {α : Type u_2} [] {z : } {a : α} :
z + 1 a z < a
@[simp]
theorem Int.one_le_ceil_iff {α : Type u_2} [] {a : α} :
1 a 0 < a
theorem Int.ceil_le_floor_add_one {α : Type u_2} [] (a : α) :
theorem Int.le_ceil {α : Type u_2} [] (a : α) :
a a
@[simp]
theorem Int.ceil_intCast {α : Type u_2} [] (z : ) :
z = z
@[simp]
theorem Int.ceil_natCast {α : Type u_2} [] (n : ) :
n = n
@[simp]
theorem Int.ceil_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
= n
theorem Int.ceil_mono {α : Type u_2} [] :
Monotone Int.ceil
theorem Int.ceil_le_ceil {α : Type u_2} [] (x : α) (y : α) :
x yx y
@[simp]
theorem Int.ceil_add_int {α : Type u_2} [] (a : α) (z : ) :
a + z = a + z
@[simp]
theorem Int.ceil_add_nat {α : Type u_2} [] (a : α) (n : ) :
a + n = a + n
@[simp]
theorem Int.ceil_add_one {α : Type u_2} [] (a : α) :
a + 1 = a + 1
@[simp]
theorem Int.ceil_add_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
@[simp]
theorem Int.ceil_sub_int {α : Type u_2} [] (a : α) (z : ) :
a - z = a - z
@[simp]
theorem Int.ceil_sub_nat {α : Type u_2} [] (a : α) (n : ) :
a - n = a - n
@[simp]
theorem Int.ceil_sub_one {α : Type u_2} [] (a : α) :
a - 1 = a - 1
@[simp]
theorem Int.ceil_sub_ofNat {α : Type u_2} [] (a : α) (n : ) [n.AtLeastTwo] :
theorem Int.ceil_lt_add_one {α : Type u_2} [] (a : α) :
a < a + 1
theorem Int.ceil_add_le {α : Type u_2} [] (a : α) (b : α) :
theorem Int.ceil_add_ceil_le {α : Type u_2} [] (a : α) (b : α) :
@[simp]
theorem Int.ceil_pos {α : Type u_2} [] {a : α} :
0 < a 0 < a
@[simp]
theorem Int.ceil_zero {α : Type u_2} [] :
@[simp]
theorem Int.ceil_one {α : Type u_2} [] :
theorem Int.ceil_nonneg {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem Int.ceil_eq_iff {α : Type u_2} [] {z : } {a : α} :
a = z z - 1 < a a z
@[simp]
theorem Int.ceil_eq_zero_iff {α : Type u_2} [] {a : α} :
a = 0 a Set.Ioc (-1) 0
theorem Int.ceil_eq_on_Ioc {α : Type u_2} [] (z : ) (a : α) :
a Set.Ioc (z - 1) za = z
theorem Int.ceil_eq_on_Ioc' {α : Type u_2} [] (z : ) (a : α) :
a Set.Ioc (z - 1) za = z
theorem Int.floor_le_ceil {α : Type u_2} [] (a : α) :
theorem Int.floor_lt_ceil_of_lt {α : Type u_2} [] {a : α} {b : α} (h : a < b) :
@[simp]
theorem Int.preimage_ceil_singleton {α : Type u_2} [] (m : ) :
Int.ceil ⁻¹' {m} = Set.Ioc (m - 1) m
theorem Int.fract_eq_zero_or_add_one_sub_ceil {α : Type u_2} [] (a : α) :
= 0 = a + 1 - a
theorem Int.ceil_eq_add_one_sub_fract {α : Type u_2} [] {a : α} (ha : 0) :
a = a + 1 -
theorem Int.ceil_sub_self_eq {α : Type u_2} [] {a : α} (ha : 0) :
a - a = 1 -

#### Intervals #

@[simp]
theorem Int.preimage_Ioo {α : Type u_2} [] {a : α} {b : α} :
Int.cast ⁻¹' Set.Ioo a b =
@[simp]
theorem Int.preimage_Ico {α : Type u_2} [] {a : α} {b : α} :
Int.cast ⁻¹' Set.Ico a b =
@[simp]
theorem Int.preimage_Ioc {α : Type u_2} [] {a : α} {b : α} :
Int.cast ⁻¹' Set.Ioc a b =
@[simp]
theorem Int.preimage_Icc {α : Type u_2} [] {a : α} {b : α} :
Int.cast ⁻¹' Set.Icc a b =
@[simp]
theorem Int.preimage_Ioi {α : Type u_2} [] {a : α} :
Int.cast ⁻¹' =
@[simp]
theorem Int.preimage_Ici {α : Type u_2} [] {a : α} :
Int.cast ⁻¹' =
@[simp]
theorem Int.preimage_Iio {α : Type u_2} [] {a : α} :
Int.cast ⁻¹' =
@[simp]
theorem Int.preimage_Iic {α : Type u_2} [] {a : α} :
Int.cast ⁻¹' =

### Round #

def round {α : Type u_2} [] (x : α) :

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

Equations
Instances For
@[simp]
theorem round_zero {α : Type u_2} [] :
= 0
@[simp]
theorem round_one {α : Type u_2} [] :
= 1
@[simp]
theorem round_natCast {α : Type u_2} [] (n : ) :
round n = n
@[simp]
theorem round_ofNat {α : Type u_2} [] (n : ) [n.AtLeastTwo] :
round () = n
@[simp]
theorem round_intCast {α : Type u_2} [] (n : ) :
round n = n
@[simp]
theorem round_add_int {α : Type u_2} [] (x : α) (y : ) :
round (x + y) = + y
@[simp]
theorem round_add_one {α : Type u_2} [] (a : α) :
round (a + 1) = + 1
@[simp]
theorem round_sub_int {α : Type u_2} [] (x : α) (y : ) :
round (x - y) = - y
@[simp]
theorem round_sub_one {α : Type u_2} [] (a : α) :
round (a - 1) = - 1
@[simp]
theorem round_add_nat {α : Type u_2} [] (x : α) (y : ) :
round (x + y) = + y
@[simp]
theorem round_add_ofNat {α : Type u_2} [] (x : α) (n : ) [n.AtLeastTwo] :
round (x + ) =
@[simp]
theorem round_sub_nat {α : Type u_2} [] (x : α) (y : ) :
round (x - y) = - y
@[simp]
theorem round_sub_ofNat {α : Type u_2} [] (x : α) (n : ) [n.AtLeastTwo] :
round (x - ) =
@[simp]
theorem round_int_add {α : Type u_2} [] (x : α) (y : ) :
round (y + x) = y +
@[simp]
theorem round_nat_add {α : Type u_2} [] (x : α) (y : ) :
round (y + x) = y +
@[simp]
theorem round_ofNat_add {α : Type u_2} [] (n : ) [n.AtLeastTwo] (x : α) :
round ( + x) =
theorem abs_sub_round_eq_min {α : Type u_2} [] (x : α) :
|x - ()| = min () (1 - )
theorem round_le {α : Type u_2} [] (x : α) (z : ) :
|x - ()| |x - z|
theorem round_eq {α : Type u_2} [] (x : α) :
= x + 1 / 2
@[simp]
theorem round_two_inv {α : Type u_2} [] :
= 1
@[simp]
theorem round_neg_two_inv {α : Type u_2} [] :
@[simp]
theorem round_eq_zero_iff {α : Type u_2} [] {x : α} :
= 0 x Set.Ico (-(1 / 2)) (1 / 2)
theorem abs_sub_round {α : Type u_2} [] (x : α) :
|x - ()| 1 / 2
theorem abs_sub_round_div_natCast_eq {α : Type u_2} [] {m : } {n : } :
|m / n - (round (m / n))| = (min (m % n) (n - m % n)) / n
theorem Nat.floor_congr {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : β} (h : ∀ (n : ), n a n b) :
theorem Nat.ceil_congr {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : β} (h : ∀ (n : ), a n b n) :
theorem Nat.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
theorem Nat.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
theorem Int.floor_congr {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : β} (h : ∀ (n : ), n a n b) :
theorem Int.ceil_congr {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : β} (h : ∀ (n : ), a n b n) :
theorem Int.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
theorem Int.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
theorem Int.map_fract {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
Int.fract (f a) = f ()
theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : ) (a : α) :
round (f a) =

#### A floor ring as a floor semiring #

@[instance 100]
instance FloorRing.toFloorSemiring {α : Type u_2} [] :
Equations
• FloorRing.toFloorSemiring = { floor := fun (a : α) => a.toNat, ceil := fun (a : α) => a.toNat, floor_of_neg := , gc_floor := , gc_ceil := }
theorem Int.floor_toNat {α : Type u_2} [] (a : α) :
theorem Int.ceil_toNat {α : Type u_2} [] (a : α) :
@[simp]
theorem Nat.floor_int :
Nat.floor = Int.toNat
@[simp]
theorem Nat.ceil_int :
Nat.ceil = Int.toNat
theorem Int.ofNat_floor_eq_floor {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem Int.ofNat_ceil_eq_ceil {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem natCast_floor_eq_intCast_floor {α : Type u_2} [] {a : α} (ha : 0 a) :
theorem natCast_ceil_eq_intCast_ceil {α : Type u_2} [] {a : α} (ha : 0 a) :
@[deprecated Int.ofNat_floor_eq_floor]
theorem Nat.cast_floor_eq_int_floor {α : Type u_2} [] {a : α} (ha : 0 a) :

Alias of Int.ofNat_floor_eq_floor.

@[deprecated Int.ofNat_ceil_eq_ceil]
theorem Nat.cast_ceil_eq_int_ceil {α : Type u_2} [] {a : α} (ha : 0 a) :

Alias of Int.ofNat_ceil_eq_ceil.

@[deprecated natCast_floor_eq_intCast_floor]
theorem Nat.cast_floor_eq_cast_int_floor {α : Type u_2} [] {a : α} (ha : 0 a) :

Alias of natCast_floor_eq_intCast_floor.

@[deprecated natCast_ceil_eq_intCast_ceil]
theorem Nat.cast_ceil_eq_cast_int_ceil {α : Type u_2} [] {a : α} (ha : 0 a) :

Alias of natCast_ceil_eq_intCast_ceil.

theorem subsingleton_floorRing {α : Type u_4} :

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

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

Instances For

Extension for the positivity tactic: Nat.ceil is positive if its input is.

Instances For

Extension for the positivity tactic: Int.ceil is positive/nonnegative if its input is.

Instances For