Documentation

Mathlib.Algebra.Order.Floor.Semiring

Lemmas on Nat.floor and Nat.ceil #

This file contains basic results on the natural-valued floor and ceiling functions.

TODO #

LinearOrderedSemiring can be relaxed to OrderedSemiring in many lemmas.

Tags #

rounding, floor, ceil

source
theorem Nat.floor_lt {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) :
⌊a⌋₊ < n ↔ a < ↑n
source
theorem Nat.floor_lt_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} (ha : 0 ≤ a) :
⌊a⌋₊ < 1 ↔ a < 1
source
theorem Nat.floor_le {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} (ha : 0 ≤ a) :
↑⌊a⌋₊ ≤ a
source
theorem Nat.floor_eq_iff {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} (ha : 0 ≤ a) :
⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
source
theorem Nat.lt_of_floor_lt {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (h : ⌊a⌋₊ < n) :
a < ↑n
source
theorem Nat.lt_one_of_floor_lt_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (h : ⌊a⌋₊ < 1) :
a < 1
source
theorem Nat.lt_succ_floor {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) :
a < ↑⌊a⌋₊.succ
source
theorem Nat.lt_floor_add_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) :
a < ↑⌊a⌋₊ + 1
source
@[simp]
theorem Nat.floor_natCast {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) :
⌊↑n⌋₊ = n
source
@[simp]
theorem Nat.floor_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
⌊0⌋₊ = 0
source
@[simp]
theorem Nat.floor_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
⌊1⌋₊ = 1
source
@[simp]
theorem Nat.floor_ofNat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
⌊OfNat.ofNat n⌋₊ = OfNat.ofNat n
source
theorem Nat.floor_of_nonpos {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : a ≤ 0) :
⌊a⌋₊ = 0
source
theorem Nat.floor_mono {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
Monotone floor
source
theorem Nat.floor_le_floor {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} [IsStrictOrderedRing R] (hab : a ≤ b) :
⌊a⌋₊ ≤ ⌊b⌋₊
source
theorem Nat.le_floor_iff' {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (hn : n ≠ 0) :
n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
source
@[simp]
theorem Nat.one_le_floor_iff {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (x : R) :
1 ≤ ⌊x⌋₊ ↔ 1 ≤ x
source
theorem Nat.floor_lt' {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (hn : n ≠ 0) :
⌊a⌋₊ < n ↔ a < ↑n
source
theorem Nat.floor_pos {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] :
0 < ⌊a⌋₊ ↔ 1 ≤ a
source
theorem Nat.pos_of_floor_pos {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (h : 0 < ⌊a⌋₊) :
0 < a
source
theorem Nat.lt_of_lt_floor {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (h : n < ⌊a⌋₊) :
↑n < a
source
theorem Nat.floor_le_of_le {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (h : a ≤ ↑n) :
⌊a⌋₊ ≤ n
source
theorem Nat.floor_le_one_of_le_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (h : a ≤ 1) :
⌊a⌋₊ ≤ 1
source
@[simp]
theorem Nat.floor_eq_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] :
⌊a⌋₊ = 0 ↔ a < 1
source
theorem Nat.floor_eq_iff' {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (hn : n ≠ 0) :
⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
source
theorem Nat.floor_eq_on_Ico {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) (a : R) :
a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋₊ = n
source
theorem Nat.floor_eq_on_Ico' {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) (a : R) :
a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋₊ = ↑n
source
@[simp]
theorem Nat.preimage_floor_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
floor ⁻¹' {0} = Set.Iio 1
source
theorem Nat.preimage_floor_of_ne_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {n : ℕ} (hn : n ≠ 0) :
floor ⁻¹' {n} = Set.Ico (↑n) (↑n + 1)

Ceil #

source
theorem Nat.add_one_le_ceil_iff {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} :
n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a
source
@[simp]
theorem Nat.one_le_ceil_iff {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} :
1 ≤ ⌈a⌉₊ ↔ 0 < a
source
theorem Nat.le_ceil {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] (a : R) :
a ≤ ↑⌈a⌉₊
source
theorem Nat.ceil_mono {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] :
Monotone ceil
source
theorem Nat.ceil_le_ceil {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} (hab : a ≤ b) :
⌈a⌉₊ ≤ ⌈b⌉₊
source
@[simp]
theorem Nat.ceil_eq_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} :
⌈a⌉₊ = 0 ↔ a ≤ 0
source
theorem Nat.ceil_eq_iff {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} (hn : n ≠ 0) :
⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n
source
@[simp]
theorem Nat.preimage_ceil_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] :
ceil ⁻¹' {0} = Set.Iic 0
source
theorem Nat.preimage_ceil_of_ne_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {n : ℕ} (hn : n ≠ 0) :
ceil ⁻¹' {n} = Set.Ioc ↑(n - 1) ↑n
source
theorem Nat.ceil_le_floor_add_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) :
⌈a⌉₊ ≤ ⌊a⌋₊ + 1
source
@[simp]
theorem Nat.ceil_intCast {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (z : ℤ) :
⌈↑z⌉₊ = z.toNat
source
@[simp]
theorem Nat.ceil_natCast {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) :
⌈↑n⌉₊ = n
source
@[simp]
theorem Nat.ceil_zero {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
⌈0⌉₊ = 0
source
@[simp]
theorem Nat.ceil_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] :
⌈1⌉₊ = 1
source
@[simp]
theorem Nat.ceil_ofNat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
⌈OfNat.ofNat n⌉₊ = OfNat.ofNat n
source
theorem Nat.lt_of_ceil_lt {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (h : ⌈a⌉₊ < n) :
a < ↑n
source
theorem Nat.le_of_ceil_le {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {n : ℕ} [IsStrictOrderedRing R] (h : ⌈a⌉₊ ≤ n) :
a ≤ ↑n
source
theorem Nat.floor_le_ceil {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a : R) :
⌊a⌋₊ ≤ ⌈a⌉₊
source
theorem Nat.floor_lt_ceil_of_lt_of_pos {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] {a b : R} (h : a < b) (h' : 0 < b) :
⌊a⌋₊ < ⌈b⌉₊

Intervals #

source
@[simp]
theorem Nat.preimage_Ioo {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} (ha : 0 ≤ a) :
Nat.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊
source
@[simp]
theorem Nat.preimage_Ico {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} :
Nat.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊
source
@[simp]
theorem Nat.preimage_Ioc {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :
Nat.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊
source
@[simp]
theorem Nat.preimage_Icc {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a b : R} (hb : 0 ≤ b) :
Nat.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊
source
@[simp]
theorem Nat.preimage_Ioi {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} (ha : 0 ≤ a) :
Nat.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊
source
@[simp]
theorem Nat.preimage_Ici {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} :
Nat.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊
source
@[simp]
theorem Nat.preimage_Iio {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} :
Nat.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊
source
@[simp]
theorem Nat.preimage_Iic {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} (ha : 0 ≤ a) :
Nat.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊
source
theorem Nat.floor_add_natCast {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) :
⌊a + ↑n⌋₊ = ⌊a⌋₊ + n
source
@[deprecated Nat.floor_add_natCast (since := "2025-04-01")]
theorem Nat.floor_add_nat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) :
⌊a + ↑n⌋₊ = ⌊a⌋₊ + n

Alias of Nat.floor_add_natCast.

source
theorem Nat.floor_add_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) :
⌊a + 1⌋₊ = ⌊a⌋₊ + 1
source
theorem Nat.floor_add_ofNat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n
source
@[simp]
theorem Nat.floor_sub_natCast {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) :
⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
source
@[deprecated Nat.floor_sub_natCast (since := "2025-04-01")]
theorem Nat.floor_sub_nat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) :
⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Alias of Nat.floor_sub_natCast.

source
@[simp]
theorem Nat.floor_sub_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) :
⌊a - 1⌋₊ = ⌊a⌋₊ - 1
source
@[simp]
theorem Nat.floor_sub_ofNat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] :
⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n
source
theorem Nat.ceil_add_natCast {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) :
⌈a + ↑n⌉₊ = ⌈a⌉₊ + n
source
@[deprecated Nat.ceil_add_natCast (since := "2025-04-01")]
theorem Nat.ceil_add_nat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) :
⌈a + ↑n⌉₊ = ⌈a⌉₊ + n

Alias of Nat.ceil_add_natCast.

source
theorem Nat.ceil_add_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) :
⌈a + 1⌉₊ = ⌈a⌉₊ + 1
source
theorem Nat.ceil_add_ofNat {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n
source
theorem Nat.ceil_lt_add_one {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} [IsStrictOrderedRing R] (ha : 0 ≤ a) :
↑⌈a⌉₊ < a + 1
source
theorem Nat.ceil_add_le {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] [IsStrictOrderedRing R] (a b : R) :
⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
source
theorem Nat.sub_one_lt_floor {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (a : R) :
a - 1 < ↑⌊a⌋₊
source
theorem Nat.floor_div_natCast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) :
⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
source
@[deprecated Nat.floor_div_natCast (since := "2025-04-01")]
theorem Nat.floor_div_nat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) :
⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Alias of Nat.floor_div_natCast.

source
theorem Nat.floor_div_ofNat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) [n.AtLeastTwo] :
⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n
source
theorem Nat.floor_div_eq_div {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (m n : ℕ) :
⌊↑m / ↑n⌋₊ = m / n

Natural division is the floor of field division.

source
theorem Nat.mul_lt_floor {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉₊ ≤ a) :
b * a < ↑⌊a⌋₊
source
theorem Nat.ceil_lt_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a) :
↑⌈a⌉₊ < b * a
source
theorem Nat.ceil_le_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a) :
↑⌈a⌉₊ ≤ b * a
source
theorem Nat.div_two_lt_floor {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 1 ≤ a) :
a / 2 < ↑⌊a⌋₊
source
theorem Nat.ceil_lt_two_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 2⁻¹ < a) :
↑⌈a⌉₊ < 2 * a
source
theorem Nat.ceil_le_two_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 2⁻¹ ≤ a) :
↑⌈a⌉₊ ≤ 2 * a
source
theorem Nat.floor_congr {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {S : Type u_3} [Semiring S] [LinearOrder S] [FloorSemiring S] {b : S} [IsStrictOrderedRing R] [IsStrictOrderedRing S] (h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b) :
⌊a⌋₊ = ⌊b⌋₊
source
theorem Nat.ceil_congr {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {a : R} {S : Type u_3} [Semiring S] [LinearOrder S] [FloorSemiring S] {b : S} (h : ∀ (n : ℕ), a ≤ ↑n ↔ b ≤ ↑n) :
⌈a⌉₊ = ⌈b⌉₊
source
theorem Nat.map_floor {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {S : Type u_3} [Semiring S] [LinearOrder S] [FloorSemiring S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] [IsStrictOrderedRing R] [IsStrictOrderedRing S] (f : F) (hf : StrictMono ⇑f) (a : R) :
⌊f a⌋₊ = ⌊a⌋₊
source
theorem Nat.map_ceil {R : Type u_1} [Semiring R] [LinearOrder R] [FloorSemiring R] {S : Type u_3} [Semiring S] [LinearOrder S] [FloorSemiring S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] (f : F) (hf : StrictMono ⇑f) (a : R) :
⌈f a⌉₊ = ⌈a⌉₊
source
theorem subsingleton_floorSemiring {R : Type u_3} [Semiring R] [LinearOrder R] :
Subsingleton (FloorSemiring R)

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