Lemmas on Int.floor, Int.ceil and Int.fract

This file contains basic results on the integer-valued floor and ceiling functions, as well as the fractional part operator.

TODO

LinearOrderedRing can be relaxed to OrderedRing in many lemmas.

Tags

rounding, floor, ceil

theorem Mathlib.Meta.Positivity.int_floor_nonneg {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} (ha : 0 ≤ a) : 0 ≤ ⌊a⌋

theorem Mathlib.Meta.Positivity.int_floor_nonneg_of_pos {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} (ha : 0 < a) : 0 ≤ ⌊a⌋

def Mathlib.Meta.Positivity.evalIntFloor : PositivityExt

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

theorem Mathlib.Meta.Positivity.nat_ceil_pos {α : Type u_1} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} : 0 < a → 0 < ⌈a⌉₊

def Mathlib.Meta.Positivity.evalNatCeil : PositivityExt

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

theorem Mathlib.Meta.Positivity.int_ceil_pos {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] {a : α} : 0 < a → 0 < ⌈a⌉

def Mathlib.Meta.Positivity.evalIntCeil : PositivityExt

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

Floor rings

Floor

theorem Int.floor_le_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : ⌊a⌋ ≤ z ↔ a < ↑z + 1

theorem Int.lt_floor_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : z < ⌊a⌋ ↔ ↑z + 1 ≤ a

@[deprecated Int.floor_lt (since := "2025-12-26")]

theorem Int.floor_le_sub_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : ⌊a⌋ ≤ z - 1 ↔ a < ↑z

@[simp]

theorem Int.floor_le_neg_one_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : ⌊a⌋ ≤ -1 ↔ a < 0

theorem Int.lt_succ_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : a < ↑⌊a⌋.succ

@[simp]

theorem Int.lt_floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : a < ↑⌊a⌋ + 1

theorem Int.floor_mono {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] : Monotone floor

theorem Int.floor_le_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} (hab : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋

theorem Int.floor_pos {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : 0 < ⌊a⌋ ↔ 1 ≤ a

theorem Int.floor_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

@[simp]

theorem Int.floor_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : ⌊a⌋ = 0 ↔ a ∈ Set.Ico 0 1

theorem Int.floor_eq_on_Ico {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (n : ℤ) (a : R) : a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋ = n

theorem Int.floor_eq_on_Ico' {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (n : ℤ) (a : R) : a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋ = ↑n

@[simp]

theorem Int.preimage_floor_singleton {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (m : ℤ) : floor ⁻¹' {m} = Set.Ico (↑m) (↑m + 1)

@[simp]

theorem Int.sub_one_lt_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : a - 1 < ↑⌊a⌋

@[simp]

theorem Int.floor_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) : ⌊↑z⌋ = z

@[simp]

theorem Int.floor_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) : ⌊↑n⌋ = ↑n

@[simp]

theorem Int.floor_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : ⌊0⌋ = 0

@[simp]

theorem Int.floor_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : ⌊1⌋ = 1

@[simp]

theorem Int.floor_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] : ⌊OfNat.ofNat n⌋ = OfNat.ofNat n

@[simp]

theorem Int.floor_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) : ⌊a + ↑z⌋ = ⌊a⌋ + z

@[simp]

theorem Int.floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌊a + 1⌋ = ⌊a⌋ + 1

theorem Int.le_floor_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

theorem Int.le_floor_add_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

@[simp]

theorem Int.floor_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) (a : R) : ⌊↑z + a⌋ = z + ⌊a⌋

@[simp]

theorem Int.floor_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) : ⌊a + ↑n⌋ = ⌊a⌋ + ↑n

@[simp]

theorem Int.floor_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n

@[simp]

theorem Int.floor_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) (a : R) : ⌊↑n + a⌋ = ↑n + ⌊a⌋

@[simp]

theorem Int.floor_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) : ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋

@[simp]

theorem Int.floor_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) : ⌊a - ↑z⌋ = ⌊a⌋ - z

@[simp]

theorem Int.floor_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) : ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

@[simp]

theorem Int.floor_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌊a - 1⌋ = ⌊a⌋ - 1

@[simp]

theorem Int.floor_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n

theorem Int.abs_sub_lt_one_of_floor_eq_floor {R : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a b : R} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1

theorem Int.floor_eq_self_iff_mem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ↑⌊a⌋ = a ↔ a ∈ Set.range Int.cast

theorem Int.floor_lt_self_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} : ↑⌊a⌋ < a ↔ a ∉ Set.range Int.cast

theorem Int.mul_cast_floor_div_cancel_of_pos {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℤ} (hn : 0 < n) (a : R) : ⌊a * ↑n⌋ / n = ⌊a⌋

theorem Int.mul_natCast_floor_div_cancel {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊a * ↑n⌋ / ↑n = ⌊a⌋

theorem Int.mul_fract_eq_one_iff_exists_int {R : Type u_4} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {x k : R} (hk : 1 < k) : k * fract x = 1 ↔ ∃ (n : ℤ), k * x = k * ↑n + 1

theorem Int.cast_mul_floor_div_cancel_of_pos {R : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℤ} (hn : 0 < n) (a : R) : ⌊↑n * a⌋ / n = ⌊a⌋

theorem Int.natCast_mul_floor_div_cancel {R : Type u_4} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊↑n * a⌋ / ↑n = ⌊a⌋

theorem Int.floor_div_cast_of_nonneg {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / ↑n⌋ = ⌊a⌋ / n

theorem Int.floor_div_natCast {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] (a : k) (n : ℕ) : ⌊a / ↑n⌋ = ⌊a⌋ / ↑n

Fractional part

@[simp]

theorem Int.self_sub_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : a - ↑⌊a⌋ = fract a

@[simp]

theorem Int.floor_add_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : ↑⌊a⌋ + fract a = a

@[simp]

theorem Int.fract_add_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : fract a + ↑⌊a⌋ = a

@[simp]

theorem Int.self_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : a - fract a = ↑⌊a⌋

@[simp]

theorem Int.fract_sub_self {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : fract a - a = -↑⌊a⌋

theorem Int.fract_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a b : R) : ∃ (z : ℤ), fract (a + b) - fract a - fract b = ↑z

@[simp]

theorem Int.fract_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℤ) : fract (a + ↑m) = fract a

@[simp]

theorem Int.fract_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℕ) : fract (a + ↑m) = fract a

@[simp]

theorem Int.fract_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract (a + 1) = fract a

@[simp]

theorem Int.fract_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : fract (a + OfNat.ofNat n) = fract a

@[simp]

theorem Int.fract_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (m : ℤ) (a : R) : fract (↑m + a) = fract a

@[simp]

theorem Int.fract_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) (a : R) : fract (↑n + a) = fract a

@[simp]

theorem Int.fract_one_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract (1 + a) = fract a

@[simp]

theorem Int.fract_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) : fract (OfNat.ofNat n + a) = fract a

@[simp]

theorem Int.fract_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (m : ℤ) : fract (a - ↑m) = fract a

@[simp]

theorem Int.fract_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) : fract (a - ↑n) = fract a

@[simp]

theorem Int.fract_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract (a - 1) = fract a

@[simp]

theorem Int.fract_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : fract (a - OfNat.ofNat n) = fract a

theorem Int.fract_add_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : fract (a + b) ≤ fract a + fract b

theorem Int.fract_add_fract_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : fract a + fract b ≤ fract (a + b) + 1

@[simp]

theorem Int.fract_nonneg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : 0 ≤ fract a

theorem Int.fract_pos {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] : 0 < fract a ↔ a ≠ ↑⌊a⌋

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

theorem Int.fract_lt_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract a < 1

@[simp]

theorem Int.fract_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : fract 0 = 0

@[simp]

theorem Int.fract_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : fract 1 = 0

theorem Int.abs_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] : |fract a| = fract a

@[simp]

theorem Int.abs_one_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] : |1 - fract a| = 1 - fract a

@[simp]

theorem Int.fract_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) : fract ↑z = 0

@[simp]

theorem Int.fract_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) : fract ↑n = 0

@[simp]

theorem Int.fract_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] : fract (OfNat.ofNat n) = 0

theorem Int.fract_floor {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract ↑⌊a⌋ = 0

@[simp]

theorem Int.floor_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌊fract a⌋ = 0

theorem Int.fract_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a b : R} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = ↑z

theorem Int.fract_eq_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a b : R} : fract a = fract b ↔ ∃ (z : ℤ), a - b = ↑z

@[simp]

theorem Int.fract_eq_self {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} : fract a = a ↔ 0 ≤ a ∧ a < 1

@[simp]

theorem Int.fract_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract (fract a) = fract a

theorem Int.fract_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} : fract a = 0 ↔ a ∈ Set.range Int.cast

theorem Int.fract_ne_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} : fract a ≠ 0 ↔ a ∉ Set.range Int.cast

theorem Int.fract_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {x : R} (hx : fract x ≠ 0) : fract (-x) = 1 - fract x

@[simp]

theorem Int.fract_neg_eq_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {x : R} : fract (-x) = 0 ↔ fract x = 0

theorem Int.fract_mul_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (b : ℕ) : ∃ (z : ℤ), fract a * ↑b - fract (a * ↑b) = ↑z

theorem Int.preimage_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (s : Set R) : fract ⁻¹' s = ⋃ (m : ℤ), (fun (x : R) => x - ↑m) ⁻¹' (s ∩ Set.Ico 0 1)

theorem Int.image_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (s : Set R) : fract '' s = ⋃ (m : ℤ), (fun (x : R) => x - ↑m) '' s ∩ Set.Ico 0 1

theorem Int.fract_div_mul_self_mem_Ico {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] (a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Set.Ico 0 a

theorem Int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [Field k] [LinearOrder k] [FloorRing k] (a b : k) (ha : a ≠ 0) : fract (b / a) * a + ⌊b / a⌋ • a = b

theorem Int.sub_floor_div_mul_nonneg {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) : 0 ≤ a - ↑⌊a / b⌋ * b

theorem Int.sub_floor_div_mul_lt {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {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} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {m n : ℕ} : fract (↑m / ↑n) = ↑(m % n) / ↑n

theorem Int.fract_div_intCast_eq_div_intCast_mod {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {m : ℤ} {n : ℕ} : fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Ceil

theorem Int.le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : z ≤ ⌈a⌉ ↔ ↑z - 1 < a

theorem Int.ceil_lt_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : ⌈a⌉ < z ↔ a ≤ ↑z - 1

@[deprecated Int.lt_ceil (since := "2025-12-26")]

theorem Int.add_one_le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : z + 1 ≤ ⌈a⌉ ↔ ↑z < a

@[simp]

theorem Int.one_le_ceil_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : 1 ≤ ⌈a⌉ ↔ 0 < a

theorem Int.ceil_le_floor_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (a : R) : ⌈a⌉ ≤ ⌊a⌋ + 1

theorem Int.ceil_mono {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] : Monotone ceil

theorem Int.ceil_le_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} (hab : a ≤ b) : ⌈a⌉ ≤ ⌈b⌉

theorem Int.ceil_nonneg_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} (ha : -1 < a) : 0 ≤ ⌈a⌉

theorem Int.ceil_eq_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {z : ℤ} {a : R} : ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z

@[simp]

theorem Int.ceil_eq_zero_iff {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : ⌈a⌉ = 0 ↔ a ∈ Set.Ioc (-1) 0

theorem Int.ceil_eq_on_Ioc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (z : ℤ) (a : R) : a ∈ Set.Ioc (↑z - 1) ↑z → ⌈a⌉ = z

@[simp]

theorem Int.preimage_ceil_singleton {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (m : ℤ) : ceil ⁻¹' {m} = Set.Ioc (↑m - 1) ↑m

theorem Int.floor_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] : ⌊-a⌋ = -⌈a⌉

theorem Int.ceil_neg {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] : ⌈-a⌉ = -⌊a⌋

@[simp]

theorem Int.ceil_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) : ⌈↑z⌉ = z

@[simp]

theorem Int.ceil_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) : ⌈↑n⌉ = ↑n

@[simp]

theorem Int.ceil_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] : ⌈OfNat.ofNat n⌉ = OfNat.ofNat n

@[simp]

theorem Int.ceil_add_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) : ⌈a + ↑z⌉ = ⌈a⌉ + z

@[simp]

theorem Int.ceil_intCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) (a : R) : ⌈↑z + a⌉ = z + ⌈a⌉

@[simp]

theorem Int.ceil_add_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) : ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

@[simp]

theorem Int.ceil_natCast_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) (a : R) : ⌈↑n + a⌉ = ↑n + ⌈a⌉

@[simp]

theorem Int.ceil_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌈a + 1⌉ = ⌈a⌉ + 1

@[simp]

theorem Int.ceil_one_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌈1 + a⌉ = 1 + ⌈a⌉

@[simp]

theorem Int.ceil_add_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n

@[simp]

theorem Int.ceil_ofNat_add {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] (a : R) : ⌈OfNat.ofNat n + a⌉ = OfNat.ofNat n + ⌈a⌉

@[simp]

theorem Int.ceil_sub_intCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (z : ℤ) : ⌈a - ↑z⌉ = ⌈a⌉ - z

@[simp]

theorem Int.ceil_sub_natCast {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) : ⌈a - ↑n⌉ = ⌈a⌉ - ↑n

@[simp]

theorem Int.ceil_sub_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌈a - 1⌉ = ⌈a⌉ - 1

@[simp]

theorem Int.ceil_sub_ofNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n

theorem Int.ceil_lt_add_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ↑⌈a⌉ < a + 1

theorem Int.ceil_add_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

theorem Int.ceil_add_ceil_le {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a b : R) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

@[simp]

theorem Int.ceil_zero {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : ⌈0⌉ = 0

@[simp]

theorem Int.ceil_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] : ⌈1⌉ = 1

theorem Int.ceil_eq_on_Ioc' {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (z : ℤ) (a : R) : a ∈ Set.Ioc (↑z - 1) ↑z → ↑⌈a⌉ = ↑z

theorem Int.ceil_eq_self_iff_mem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ↑⌈a⌉ = a ↔ a ∈ Set.range Int.cast

theorem Int.floor_le_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌊a⌋ ≤ ⌈a⌉

theorem Int.floor_lt_ceil_of_lt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉

theorem Int.ceil_eq_floor_add_one_iff_notMem {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast

theorem Int.fract_eq_zero_or_add_one_sub_ceil {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] (a : R) : fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

theorem Int.ceil_eq_add_one_sub_fract {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] (ha : fract a ≠ 0) : ↑⌈a⌉ = a + 1 - fract a

theorem Int.ceil_sub_self_eq {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} [IsStrictOrderedRing R] (ha : fract a ≠ 0) : ↑⌈a⌉ - a = 1 - fract a

theorem Int.mul_lt_floor {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉ ≤ a) : b * a < ↑⌊a⌋

theorem Int.ceil_div_ceil_inv_sub_one {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) : ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

theorem Int.ceil_lt_mul {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b < a) : ↑⌈a⌉ < b * a

theorem Int.ceil_le_mul {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a) : ↑⌈a⌉ ≤ b * a

theorem Int.div_two_lt_floor {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a : k} (ha : 1 ≤ a) : a / 2 < ↑⌊a⌋

theorem Int.ceil_lt_two_mul {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ < a) : ↑⌈a⌉ < 2 * a

theorem Int.ceil_le_two_mul {k : Type u_4} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a : k} (ha : 2⁻¹ ≤ a) : ↑⌈a⌉ ≤ 2 * a

Intervals

@[simp]

theorem Int.preimage_Ioo {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} : Int.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉

@[simp]

theorem Int.preimage_Ico {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} : Int.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉

@[simp]

theorem Int.preimage_Ioc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} : Int.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋

@[simp]

theorem Int.preimage_Icc {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a b : R} : Int.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋

@[simp]

theorem Int.preimage_Ioi {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : Int.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋

@[simp]

theorem Int.preimage_Ici {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : Int.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉

@[simp]

theorem Int.preimage_Iio {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : Int.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉

@[simp]

theorem Int.preimage_Iic {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] {a : R} : Int.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋

theorem Int.floor_congr {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] {a : R} {b : S} (h : ∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b) : ⌊a⌋ = ⌊b⌋

theorem Int.ceil_congr {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] {a : R} {b : S} (h : ∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n) : ⌈a⌉ = ⌈b⌉

theorem Int.map_floor {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) : ⌊f a⌋ = ⌊a⌋

theorem Int.map_ceil {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) : ⌈f a⌉ = ⌈a⌉

theorem Int.map_fract {F : Type u_1} {R : Type u_2} {S : Type u_3} [Ring R] [LinearOrder R] [Ring S] [LinearOrder S] [FloorRing R] [FloorRing S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) : fract (f a) = f (fract a)

theorem Nat.ceil_lt_add_one_of_gt_neg_one {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R] {a : R} (ha : -1 < a) : ↑⌈a⌉₊ < a + 1

a variant of Nat.ceil_lt_add_one with its condition 0 ≤ a generalized to -1 < a

A floor ring as a floor semiring

theorem Int.natCast_floor_eq_floor {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : 0 ≤ a) : ↑⌊a⌋₊ = ⌊a⌋

theorem Int.natCast_ceil_eq_ceil {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : 0 ≤ a) : ↑⌈a⌉₊ = ⌈a⌉

theorem Int.natCast_ceil_eq_ceil_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : -1 < a) : ↑⌈a⌉₊ = ⌈a⌉

theorem natCast_floor_eq_intCast_floor {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : 0 ≤ a) : ↑⌊a⌋₊ = ↑⌊a⌋

theorem natCast_ceil_eq_intCast_ceil {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : 0 ≤ a) : ↑⌈a⌉₊ = ↑⌈a⌉

theorem natCast_ceil_eq_intCast_ceil_of_neg_one_lt {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R} (ha : -1 < a) : ↑⌈a⌉₊ = ↑⌈a⌉

theorem subsingleton_floorRing {R : Type u_4} [Ring R] [LinearOrder R] : Subsingleton (FloorRing R)

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