doc-next-gen

Mathlib.Algebra.Order.Floor.Semiring

Module docstring

{"# 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 ","#### Ceil ","#### Intervals "}

Nat.floor_lt theorem
(ha : 0 ≤ a) : ⌊a⌋₊ < n ↔ a < n
Full source 
theorem floor_lt (ha : 0 ≤ a) : ⌊a⌋₊⌊a⌋₊ < n ↔ a < n :=
  lt_iff_lt_of_le_iff_le <| le_floor_iff ha
Floor Comparison: $\lfloor a \rfloor < n \leftrightarrow a < n$ for $a \geq 0$
Informal description
For any real number $a \geq 0$ and natural number $n$, the floor of $a$ (denoted $\lfloor a \rfloor$) is less than $n$ if and only if $a$ is less than $n$. That is, $\lfloor a \rfloor < n \leftrightarrow a < n$.
Nat.floor_lt_one theorem
(ha : 0 ≤ a) : ⌊a⌋₊ < 1 ↔ a < 1
Full source 
theorem floor_lt_one (ha : 0 ≤ a) : ⌊a⌋₊⌊a⌋₊ < 1 ↔ a < 1 :=
  (floor_lt ha).trans <| by rw [Nat.cast_one]
Floor Comparison with One: $\lfloor a \rfloor < 1 \leftrightarrow a < 1$ for $a \geq 0$
Informal description
For any real number $a \geq 0$, the floor of $a$ (denoted $\lfloor a \rfloor$) is less than $1$ if and only if $a$ is less than $1$. That is, $\lfloor a \rfloor < 1 \leftrightarrow a < 1$.
Nat.floor_le theorem
(ha : 0 ≤ a) : (⌊a⌋₊ : R) ≤ a
Full source 
theorem floor_le (ha : 0 ≤ a) : (⌊a⌋₊ : R) ≤ a :=
  (le_floor_iff ha).1 le_rfl
Floor Lower Bound: $\lfloor a \rfloor \leq a$ for $a \geq 0$
Informal description
For any real number $a \geq 0$, the floor of $a$ (denoted $\lfloor a \rfloor$) satisfies $\lfloor a \rfloor \leq a$.
Nat.floor_eq_iff theorem
(ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
Full source 
theorem floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by
  rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
Floor Characterization: $\lfloor a \rfloor = n \leftrightarrow n \leq a < n+1$ for $a \geq 0$
Informal description
For any real number $a \geq 0$ and natural number $n$, the floor of $a$ equals $n$ if and only if $a$ lies in the interval $[n, n+1)$. That is, $\lfloor a \rfloor = n \leftrightarrow n \leq a < n+1$.
Nat.lt_of_floor_lt theorem
(h : ⌊a⌋₊ < n) : a < n
Full source 
theorem lt_of_floor_lt (h : ⌊a⌋₊ < n) : a < n :=
  lt_of_not_le fun h' => (le_floor h').not_lt h
Natural Floor Strict Inequality Implies Original Strict Inequality
Informal description
For any real number $a \geq 0$ and natural number $n$, if the natural floor of $a$ (denoted $\lfloor a \rfloor$) is less than $n$, then $a < n$.
Nat.lt_one_of_floor_lt_one theorem
(h : ⌊a⌋₊ < 1) : a < 1
Full source 
theorem lt_one_of_floor_lt_one (h : ⌊a⌋₊ < 1) : a < 1 := mod_cast lt_of_floor_lt h
Floor Less Than One Implies Value Less Than One
Informal description
For any real number $a \geq 0$, if the natural floor of $a$ (denoted $\lfloor a \rfloor$) is less than $1$, then $a < 1$.
Nat.lt_succ_floor theorem
(a : R) : a < ⌊a⌋₊.succ
Full source 
theorem lt_succ_floor (a : R) : a < ⌊a⌋₊.succ :=
  lt_of_floor_lt <| Nat.lt_succ_self _
Upper bound for real numbers via floor successor: $a < \lfloor a \rfloor + 1$
Informal description
For any real number $a \geq 0$ in a linearly ordered semiring $R$, the value $a$ is strictly less than the successor of its natural floor, i.e., $a < \lfloor a \rfloor + 1$.
Nat.lt_floor_add_one theorem
(a : R) : a < ⌊a⌋₊ + 1
Full source 
@[bound]
theorem lt_floor_add_one (a : R) : a < ⌊a⌋₊ + 1 := by simpa using lt_succ_floor a
Upper bound via floor: $a < \lfloor a \rfloor + 1$
Informal description
For any real number $a \geq 0$ in a linearly ordered semiring $R$, the value $a$ is strictly less than one plus its natural floor, i.e., $a < \lfloor a \rfloor + 1$.
Nat.floor_natCast theorem
(n : ℕ) : ⌊(n : R)⌋₊ = n
Full source 
@[simp]
theorem floor_natCast (n : ℕ) : ⌊(n : R)⌋₊ = n :=
  eq_of_forall_le_iff fun a => by
    rw [le_floor_iff, Nat.cast_le]
    exact n.cast_nonneg
Floor of Natural Number is Itself
Informal description
For any natural number $n$, the floor of $n$ (viewed as an element of a linearly ordered semiring $R$) is equal to $n$ itself, i.e., $\lfloor n \rfloor = n$.
Nat.floor_zero theorem
: ⌊(0 : R)⌋₊ = 0
Full source 
@[simp]
theorem floor_zero : ⌊(0 : R)⌋₊ = 0 := by rw [← Nat.cast_zero, floor_natCast]
Floor of Zero is Zero
Informal description
The floor of zero in any linearly ordered semiring $R$ is zero, i.e., $\lfloor 0 \rfloor = 0$.
Nat.floor_one theorem
: ⌊(1 : R)⌋₊ = 1
Full source 
@[simp]
theorem floor_one : ⌊(1 : R)⌋₊ = 1 := by rw [← Nat.cast_one, floor_natCast]
Floor of One is One
Informal description
For any linearly ordered semiring $R$, the floor of the element $1 \in R$ is equal to $1$, i.e., $\lfloor 1 \rfloor = 1$.
Nat.floor_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ⌊(ofNat(n) : R)⌋₊ = ofNat(n)
Full source 
@[simp]
theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊(ofNat(n) : R)⌋₊ = ofNat(n) :=
  Nat.floor_natCast _
Floor of Numeric Literal (n ≥ 2) is Itself
Informal description
For any natural number $n$ (with $n \geq 2$), the floor of the numeral `ofNat(n)` in a linearly ordered semiring $R$ is equal to `ofNat(n)` itself, i.e., $\lfloor \text{ofNat}(n) \rfloor = \text{ofNat}(n)$.
Nat.floor_of_nonpos theorem
(ha : a ≤ 0) : ⌊a⌋₊ = 0
Full source 
theorem floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
  ha.lt_or_eq.elim FloorSemiring.floor_of_neg <| by
    rintro rfl
    exact floor_zero
Floor of Nonpositive Element is Zero
Informal description
For any element $a$ in a linearly ordered semiring $R$ such that $a \leq 0$, the floor of $a$ is equal to $0$, i.e., $\lfloor a \rfloor = 0$.
Nat.floor_mono theorem
: Monotone (floor : R → ℕ)
Full source 
theorem floor_mono : Monotone (floor : R → ℕ) := fun a b h => by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact le_floor ((floor_le ha).trans h)
Monotonicity of the Floor Function
Informal description
The floor function $\lfloor \cdot \rfloor : R \to \mathbb{N}$ is monotone, meaning that for any $a, b \in R$, if $a \leq b$ then $\lfloor a \rfloor \leq \lfloor b \rfloor$.
Nat.floor_le_floor theorem
(hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊
Full source 
@[gcongr, bound] lemma floor_le_floor (hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊ := floor_mono hab
Monotonicity of Floor Function: $a \leq b \Rightarrow \lfloor a \rfloor \leq \lfloor b \rfloor$
Informal description
For any elements $a$ and $b$ in a linearly ordered semiring $R$, if $a \leq b$ then $\lfloor a \rfloor \leq \lfloor b \rfloor$, where $\lfloor \cdot \rfloor$ denotes the floor function mapping $R$ to $\mathbb{N}$.
Nat.le_floor_iff' theorem
(hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : R) ≤ a
Full source 
theorem le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : R) ≤ a := by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact
      iff_of_false (Nat.pos_of_ne_zero hn).not_le
        (not_le_of_lt <| ha.trans_lt <| cast_pos.2 <| Nat.pos_of_ne_zero hn)
  · exact le_floor_iff ha
Natural Number Comparison with Floor: $n \leq \lfloor a \rfloor \leftrightarrow n \leq a$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$ and any element $a$ in a linearly ordered semiring $R$, the inequality $n \leq \lfloor a \rfloor$ holds if and only if the cast of $n$ to $R$ is less than or equal to $a$, i.e., $n \leq \lfloor a \rfloor \leftrightarrow (n : R) \leq a$.
Nat.one_le_floor_iff theorem
(x : R) : 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x
Full source 
@[simp]
theorem one_le_floor_iff (x : R) : 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x :=
  mod_cast le_floor_iff' one_ne_zero
Floor Comparison at One: $1 \leq \lfloor x \rfloor \leftrightarrow 1 \leq x$
Informal description
For any element $x$ in a linearly ordered semiring $R$, the inequality $1 \leq \lfloor x \rfloor$ holds if and only if $1 \leq x$, where $\lfloor \cdot \rfloor$ denotes the floor function mapping $R$ to $\mathbb{N}$.
Nat.floor_lt' theorem
(hn : n ≠ 0) : ⌊a⌋₊ < n ↔ a < n
Full source 
theorem floor_lt' (hn : n ≠ 0) : ⌊a⌋₊⌊a⌋₊ < n ↔ a < n :=
  lt_iff_lt_of_le_iff_le <| le_floor_iff' hn
Floor Comparison: $\lfloor a \rfloor < n \leftrightarrow a < n$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$ and any element $a$ in a linearly ordered semiring $R$, the floor of $a$ is less than $n$ if and only if $a$ is less than $n$, i.e., $\lfloor a \rfloor < n \leftrightarrow a < n$.
Nat.pos_of_floor_pos theorem
(h : 0 < ⌊a⌋₊) : 0 < a
Full source 
theorem pos_of_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
  (le_or_lt a 0).resolve_left fun ha => lt_irrefl 0 <| by rwa [floor_of_nonpos ha] at h
Positivity of Floor Implies Positivity of Element
Informal description
For any element $a$ in a linearly ordered semiring $R$, if the floor of $a$ is positive (i.e., $\lfloor a \rfloor > 0$), then $a$ itself is positive (i.e., $a > 0$).
Nat.lt_of_lt_floor theorem
(h : n < ⌊a⌋₊) : ↑n < a
Full source 
theorem lt_of_lt_floor (h : n < ⌊a⌋₊) : ↑n < a :=
  (Nat.cast_lt.2 h).trans_le <| floor_le (pos_of_floor_pos <| (Nat.zero_le n).trans_lt h).le
Natural Number Less Than Floor Implies Less Than Element ($n < \lfloor a \rfloor \Rightarrow n < a$)
Informal description
For any natural number $n$ and real number $a$, if $n$ is less than the floor of $a$ (i.e., $n < \lfloor a \rfloor$), then $n$ is less than $a$ (i.e., $n < a$).
Nat.floor_le_of_le theorem
(h : a ≤ n) : ⌊a⌋₊ ≤ n
Full source 
theorem floor_le_of_le (h : a ≤ n) : ⌊a⌋₊ ≤ n :=
  le_imp_le_iff_lt_imp_lt.2 lt_of_lt_floor h
Floor Bounded by Natural Number ($a \leq n \Rightarrow \lfloor a \rfloor \leq n$)
Informal description
For any real number $a$ and natural number $n$, if $a \leq n$, then the floor of $a$ is less than or equal to $n$, i.e., $\lfloor a \rfloor \leq n$.
Nat.floor_le_one_of_le_one theorem
(h : a ≤ 1) : ⌊a⌋₊ ≤ 1
Full source 
theorem floor_le_one_of_le_one (h : a ≤ 1) : ⌊a⌋₊ ≤ 1 :=
  floor_le_of_le <| h.trans_eq <| Nat.cast_one.symm
Floor Bound for $a \leq 1$: $\lfloor a \rfloor \leq 1$
Informal description
For any real number $a$ such that $a \leq 1$, the floor of $a$ is less than or equal to $1$, i.e., $\lfloor a \rfloor \leq 1$.
Nat.floor_eq_zero theorem
: ⌊a⌋₊ = 0 ↔ a < 1
Full source 
@[simp]
theorem floor_eq_zero : ⌊a⌋₊⌊a⌋₊ = 0 ↔ a < 1 := by
  rw [← lt_one_iff, ← @cast_one R]
  exact floor_lt' Nat.one_ne_zero
Floor Equals Zero if and only if Less Than One
Informal description
For any element $a$ in a linearly ordered semiring $R$, the floor of $a$ equals zero if and only if $a$ is less than $1$, i.e., $\lfloor a \rfloor = 0 \leftrightarrow a < 1$.
Nat.floor_eq_iff' theorem
(hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
Full source 
theorem floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by
  rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
Floor Characterization: $\lfloor a \rfloor = n \leftrightarrow n \leq a < n + 1$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$ and any element $a$ in a linearly ordered semiring $R$, the floor of $a$ equals $n$ if and only if the cast of $n$ to $R$ is less than or equal to $a$ and $a$ is strictly less than $n+1$ (also cast to $R$), i.e., $\lfloor a \rfloor = n \leftrightarrow n \leq a < n + 1$.
Nat.floor_eq_on_Ico theorem
(n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set R), ⌊a⌋₊ = n
Full source 
theorem floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set R), ⌊a⌋₊ = n := fun _ ⟨h₀, h₁⟩ =>
  (floor_eq_iff <| n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩
Floor Function on Interval $[n, n+1)$ is Constant $n$
Informal description
For any natural number $n$ and any real number $a$ in the interval $[n, n+1)$, the floor of $a$ equals $n$, i.e., $\lfloor a \rfloor = n$.
Nat.floor_eq_on_Ico' theorem
(n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set R), (⌊a⌋₊ : R) = n
Full source 
theorem floor_eq_on_Ico' (n : ℕ) :
    ∀ a ∈ (Set.Ico n (n + 1) : Set R), (⌊a⌋₊ : R) = n :=
  fun x hx => mod_cast floor_eq_on_Ico n x hx
Floor function identity on $[n, n+1)$ with real-valued equality
Informal description
For any natural number $n$ and any real number $a$ in the interval $[n, n+1)$, the floor of $a$ (considered as a real number via the canonical embedding) equals $n$, i.e., $\lfloor a \rfloor = n$ where both sides are viewed in $\mathbb{R}$.
Nat.preimage_floor_zero theorem
: (floor : R → ℕ) ⁻¹' {0} = Iio 1
Full source 
@[simp]
theorem preimage_floor_zero : (floor : R → ℕ) ⁻¹' {0} = Iio 1 :=
  ext fun _ => floor_eq_zero
Preimage of Zero under Floor Function Equals $(-\infty, 1)$
Informal description
The preimage of the singleton set $\{0\}$ under the floor function $\lfloor \cdot \rfloor : R \to \mathbb{N}$ is equal to the interval $(-\infty, 1)$, i.e., $\{a \in R \mid \lfloor a \rfloor = 0\} = \{a \in R \mid a < 1\}$.
Nat.preimage_floor_of_ne_zero theorem
{n : ℕ} (hn : n ≠ 0) : (floor : R → ℕ) ⁻¹' { n } = Ico (n : R) (n + 1)
Full source 
theorem preimage_floor_of_ne_zero {n : ℕ} (hn : n ≠ 0) :
    (floor : R → ℕ) ⁻¹' {n} = Ico (n : R) (n + 1) :=
  ext fun _ => floor_eq_iff' hn
Preimage Characterization of Floor Function for Nonzero Natural Numbers
Informal description
For any nonzero natural number $n$ and any real number $a$, the preimage of the singleton set $\{n\}$ under the floor function $\lfloor \cdot \rfloor$ is equal to the interval $[n, n+1)$, i.e., $\lfloor a \rfloor = n$ if and only if $a \in [n, n+1)$.
Nat.add_one_le_ceil_iff theorem
: n + 1 ≤ ⌈a⌉₊ ↔ (n : R) < a
Full source 
theorem add_one_le_ceil_iff : n + 1 ≤ ⌈a⌉₊ ↔ (n : R) < a := by
  rw [← Nat.lt_ceil, Nat.add_one_le_iff]
Ceiling Lower Bound: $n + 1 \leq \lceil a \rceil \leftrightarrow n < a$
Informal description
For any real number $a$ and natural number $n$, the inequality $n + 1 \leq \lceil a \rceil$ holds if and only if $n < a$ (where $n$ is considered as a real number via the canonical embedding).
Nat.le_ceil theorem
(a : R) : a ≤ ⌈a⌉₊
Full source 
@[bound]
theorem le_ceil (a : R) : a ≤ ⌈a⌉₊ :=
  ceil_le.1 le_rfl
Ceiling Lower Bound: $a \leq \lceil a \rceil$
Informal description
For any real number $a$, the ceiling of $a$ (denoted $\lceil a \rceil$) is greater than or equal to $a$ itself, i.e., $a \leq \lceil a \rceil$.
Nat.ceil_mono theorem
: Monotone (ceil : R → ℕ)
Full source 
theorem ceil_mono : Monotone (ceil : R → ℕ) :=
  gc_ceil_coe.monotone_l
Monotonicity of the Ceiling Function
Informal description
The ceiling function $\lceil \cdot \rceil : R \to \mathbb{N}$ is monotone, meaning that for any $a, b \in R$, if $a \leq b$ then $\lceil a \rceil \leq \lceil b \rceil$.
Nat.ceil_le_ceil theorem
(hab : a ≤ b) : ⌈a⌉₊ ≤ ⌈b⌉₊
Full source 
@[gcongr, bound] lemma ceil_le_ceil (hab : a ≤ b) : ⌈a⌉₊ ≤ ⌈b⌉₊ := ceil_mono hab
Monotonicity of Ceiling Function: $a \leq b \Rightarrow \lceil a \rceil \leq \lceil b \rceil$
Informal description
For any real numbers $a$ and $b$ such that $a \leq b$, the ceiling of $a$ is less than or equal to the ceiling of $b$, i.e., $\lceil a \rceil \leq \lceil b \rceil$.
Nat.ceil_eq_iff theorem
(hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n
Full source 
theorem ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n := by
  rw [← ceil_le, ← not_le, ← ceil_le, not_le,
    tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
    le_antisymm_iff, and_comm]
Characterization of Ceiling Function: $\lceil a \rceil = n \leftrightarrow n-1 < a \leq n$ for $n \neq 0$
Informal description
For any real number $a$ and nonzero natural number $n$, the ceiling of $a$ equals $n$ if and only if $a$ lies in the interval $(n-1, n]$. In other words, $\lceil a \rceil = n \leftrightarrow n-1 < a \leq n$.
Nat.preimage_ceil_zero theorem
: (Nat.ceil : R → ℕ) ⁻¹' {0} = Iic 0
Full source 
@[simp]
theorem preimage_ceil_zero : (Nat.ceil : R → ℕ) ⁻¹' {0} = Iic 0 :=
  ext fun _ => ceil_eq_zero
Preimage of Zero under Ceiling Function Equals Nonpositive Reals
Informal description
The preimage of the singleton set $\{0\}$ under the natural-valued ceiling function $\lceil \cdot \rceil : \mathbb{R} \to \mathbb{N}$ is equal to the left-infinite right-closed interval $(-\infty, 0]$. In other words, $\{x \in \mathbb{R} \mid \lceil x \rceil = 0\} = (-\infty, 0]$.
Nat.preimage_ceil_of_ne_zero theorem
(hn : n ≠ 0) : (Nat.ceil : R → ℕ) ⁻¹' { n } = Ioc (↑(n - 1) : R) n
Full source 
theorem preimage_ceil_of_ne_zero (hn : n ≠ 0) : (Nat.ceil : R → ℕ) ⁻¹' {n} = Ioc (↑(n - 1) : R) n :=
  ext fun _ => ceil_eq_iff hn
Preimage Characterization of Ceiling Function: $\lceil \cdot \rceil^{-1}\{n\} = (n-1, n]$ for $n \neq 0$
Informal description
For any nonzero natural number $n$, the preimage of the singleton set $\{n\}$ under the natural-valued ceiling function $\lceil \cdot \rceil : \mathbb{R} \to \mathbb{N}$ is equal to the left-open right-closed interval $(n-1, n]$. In other words, $\{x \in \mathbb{R} \mid \lceil x \rceil = n\} = (n-1, n]$.
Nat.ceil_le_floor_add_one theorem
(a : R) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1
Full source 
@[bound]
theorem ceil_le_floor_add_one (a : R) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1 := by
  rw [ceil_le, Nat.cast_add, Nat.cast_one]
  exact (lt_floor_add_one a).le
Ceiling-Floor Inequality: $\lceil a \rceil \leq \lfloor a \rfloor + 1$
Informal description
For any real number $a \geq 0$ in a linearly ordered semiring $R$, the ceiling of $a$ is less than or equal to one plus the floor of $a$, i.e., $\lceil a \rceil \leq \lfloor a \rfloor + 1$.
Nat.ceil_intCast theorem
{R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (z : ℤ) : ⌈(z : R)⌉₊ = z.toNat
Full source 
@[simp]
theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
    [FloorSemiring R] (z : ℤ) :
    ⌈(z : R)⌉₊ = z.toNat :=
  eq_of_forall_ge_iff fun a => by
    simp only [ceil_le, Int.toNat_le]
    norm_cast
Ceiling of Integer Cast Equals Non-Negative Part
Informal description
Let $R$ be a linearly ordered ring with a strict order and a floor function. For any integer $z$, the ceiling of the cast of $z$ in $R$ is equal to the natural number obtained by truncating $z$ to its non-negative part, i.e., $\lceil z \rceil = z_{\geq 0}$ where $z_{\geq 0}$ is $z$ if $z \geq 0$ and $0$ otherwise.
Nat.ceil_natCast theorem
(n : ℕ) : ⌈(n : R)⌉₊ = n
Full source 
@[simp]
theorem ceil_natCast (n : ℕ) : ⌈(n : R)⌉₊ = n :=
  eq_of_forall_ge_iff fun a => by rw [ceil_le, cast_le]
Ceiling of Natural Number Cast in Ordered Semiring
Informal description
For any natural number $n$ and any ordered semiring $R$ with a floor function, the ceiling of $n$ (viewed as an element of $R$) is equal to $n$ itself, i.e., $\lceil n \rceil = n$.
Nat.ceil_zero theorem
: ⌈(0 : R)⌉₊ = 0
Full source 
@[simp]
theorem ceil_zero : ⌈(0 : R)⌉₊ = 0 := by rw [← Nat.cast_zero, ceil_natCast]
Ceiling of Zero
Informal description
The ceiling of $0$ in any ordered semiring $R$ with a floor function is $0$, i.e., $\lceil 0 \rceil = 0$.
Nat.ceil_one theorem
: ⌈(1 : R)⌉₊ = 1
Full source 
@[simp]
theorem ceil_one : ⌈(1 : R)⌉₊ = 1 := by rw [← Nat.cast_one, ceil_natCast]
Ceiling of One in Ordered Semiring
Informal description
For any ordered semiring $R$ with a ceiling function, the ceiling of the multiplicative identity element $1$ in $R$ is equal to $1$ itself, i.e., $\lceil 1 \rceil = 1$.
Nat.ceil_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ⌈(ofNat(n) : R)⌉₊ = ofNat(n)
Full source 
@[simp]
theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(ofNat(n) : R)⌉₊ = ofNat(n) := ceil_natCast n
Ceiling of Numerals $\geq 2$ in Ordered Semiring
Informal description
For any natural number $n \geq 2$ and any ordered semiring $R$ with a ceiling function, the ceiling of the numeral $n$ (viewed as an element of $R$) is equal to $n$ itself, i.e., $\lceil n \rceil = n$.
Nat.lt_of_ceil_lt theorem
(h : ⌈a⌉₊ < n) : a < n
Full source 
theorem lt_of_ceil_lt (h : ⌈a⌉₊ < n) : a < n :=
  (le_ceil a).trans_lt (Nat.cast_lt.2 h)
Ceiling Bound Implies Original Bound: $\lceil a \rceil < n \implies a < n$
Informal description
For any real number $a$ and natural number $n$, if the ceiling of $a$ (denoted $\lceil a \rceil$) is less than $n$, then $a$ is also less than $n$, i.e., $\lceil a \rceil < n \implies a < n$.
Nat.le_of_ceil_le theorem
(h : ⌈a⌉₊ ≤ n) : a ≤ n
Full source 
theorem le_of_ceil_le (h : ⌈a⌉₊ ≤ n) : a ≤ n :=
  (le_ceil a).trans (Nat.cast_le.2 h)
Ceiling Implies Upper Bound: $\lceil a \rceil \leq n \Rightarrow a \leq n$
Informal description
For any real number $a$ and natural number $n$, if the ceiling of $a$ (denoted $\lceil a \rceil$) is less than or equal to $n$, then $a \leq n$.
Nat.floor_le_ceil theorem
(a : R) : ⌊a⌋₊ ≤ ⌈a⌉₊
Full source 
@[bound]
theorem floor_le_ceil (a : R) : ⌊a⌋₊ ≤ ⌈a⌉₊ := by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact cast_le.1 ((floor_le ha).trans <| le_ceil _)
Floor-Ceiling Inequality: $\lfloor a \rfloor \leq \lceil a \rceil$
Informal description
For any real number $a$, the floor of $a$ is less than or equal to its ceiling, i.e., $\lfloor a \rfloor \leq \lceil a \rceil$.
Nat.floor_lt_ceil_of_lt_of_pos theorem
{a b : R} (h : a < b) (h' : 0 < b) : ⌊a⌋₊ < ⌈b⌉₊
Full source 
theorem floor_lt_ceil_of_lt_of_pos {a b : R} (h : a < b) (h' : 0 < b) : ⌊a⌋₊ < ⌈b⌉₊ := by
  rcases le_or_lt 0 a with (ha | ha)
  · rw [floor_lt ha]
    exact h.trans_le (le_ceil _)
  · rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]
Floor-Ceiling Inequality for Positive Intervals: $\lfloor a \rfloor < \lceil b \rceil$ when $a < b$ and $b > 0$
Informal description
For any real numbers $a$ and $b$ such that $a < b$ and $0 < b$, the floor of $a$ is strictly less than the ceiling of $b$, i.e., $\lfloor a \rfloor < \lceil b \rceil$.
Nat.preimage_Ioo theorem
{a b : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊
Full source 
@[simp]
theorem preimage_Ioo {a b : R} (ha : 0 ≤ a) :
    (Nat.cast : ℕ → R) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊ := by
  ext
  simp [floor_lt, lt_ceil, ha]
Preimage of Open Interval under Natural Embedding Equals Floor-Ceiling Interval
Informal description
For any real numbers $a$ and $b$ with $a \geq 0$, the preimage of the open interval $(a, b)$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the open interval $(\lfloor a \rfloor, \lceil b \rceil)$ in $\mathbb{N}$, where $\lfloor \cdot \rfloor$ and $\lceil \cdot \rceil$ denote the floor and ceiling functions respectively.
Nat.preimage_Ico theorem
{a b : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊
Full source 
@[simp]
theorem preimage_Ico {a b : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊ := by
  ext
  simp [ceil_le, lt_ceil]
Preimage of Left-Closed Right-Open Interval under Natural Embedding via Ceiling Function
Informal description
For any real numbers $a$ and $b$, the preimage of the interval $[a, b)$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the interval $[\lceil a \rceil, \lceil b \rceil)$ in $\mathbb{N}$, where $\lceil \cdot \rceil$ denotes the ceiling function. In other words: $\{n \in \mathbb{N} \mid a \leq n < b\} = \{n \in \mathbb{N} \mid \lceil a \rceil \leq n < \lceil b \rceil\}$
Nat.preimage_Ioc theorem
{a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊
Full source 
@[simp]
theorem preimage_Ioc {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    (Nat.cast : ℕ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊ := by
  ext
  simp [floor_lt, le_floor_iff, hb, ha]
Preimage of Ioc Interval under Natural Embedding Equals Ioc of Floor Values
Informal description
For any real numbers $a$ and $b$ with $a \geq 0$ and $b \geq 0$, the preimage of the left-open right-closed interval $(a, b]$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the left-open right-closed interval $(\lfloor a \rfloor_\mathbb{N}, \lfloor b \rfloor_\mathbb{N}]$ of natural numbers.
Nat.preimage_Icc theorem
{a b : R} (hb : 0 ≤ b) : (Nat.cast : ℕ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊
Full source 
@[simp]
theorem preimage_Icc {a b : R} (hb : 0 ≤ b) :
    (Nat.cast : ℕ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊ := by
  ext
  simp [ceil_le, hb, le_floor_iff]
Preimage of Closed Interval under Natural Embedding Equals Ceiling-Floor Interval
Informal description
For any real numbers $a$ and $b$ with $b \geq 0$, the preimage of the closed interval $[a, b]$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the closed interval $[\lceil a \rceil, \lfloor b \rfloor]$ in $\mathbb{N}$, where $\lceil \cdot \rceil$ and $\lfloor \cdot \rfloor$ denote the ceiling and floor functions respectively.
Nat.preimage_Ioi theorem
{a : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊
Full source 
@[simp]
theorem preimage_Ioi {a : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊ := by
  ext
  simp [floor_lt, ha]
Preimage of Right-Infinite Interval under Natural Embedding Equals Floor-Based Interval
Informal description
For any real number $a \geq 0$, the preimage of the open interval $(a, \infty)$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the open interval $(\lfloor a \rfloor, \infty)$ in $\mathbb{N}$, where $\lfloor a \rfloor$ denotes the floor of $a$ as a natural number.
Nat.preimage_Ici theorem
{a : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊
Full source 
@[simp]
theorem preimage_Ici {a : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊ := by
  ext
  simp [ceil_le]
Preimage of Right-Infinite Interval under Natural Embedding Equals Ceiling Interval
Informal description
For any real number $a$, the preimage of the interval $[a, \infty)$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the interval $[\lceil a \rceil, \infty)$ in $\mathbb{N}$, where $\lceil a \rceil$ denotes the ceiling of $a$ (the smallest natural number greater than or equal to $a$).
Nat.preimage_Iio theorem
{a : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊
Full source 
@[simp]
theorem preimage_Iio {a : R} : (Nat.cast : ℕ → R) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊ := by
  ext
  simp [lt_ceil]
Preimage of $(-\infty, a)$ under natural embedding equals $(-\infty, \lceil a \rceil)$ in $\mathbb{N}$
Informal description
For any real number $a$ and the canonical embedding $\mathbb{N} \to \mathbb{R}$, the preimage of the open interval $(-\infty, a)$ under this embedding is equal to the open interval $(-\infty, \lceil a \rceil)$ in $\mathbb{N}$, where $\lceil a \rceil$ denotes the ceiling of $a$.
Nat.preimage_Iic theorem
{a : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊
Full source 
@[simp]
theorem preimage_Iic {a : R} (ha : 0 ≤ a) : (Nat.cast : ℕ → R) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊ := by
  ext
  simp [le_floor_iff, ha]
Preimage of Closed Interval under Natural Number Embedding Equals Floor Interval
Informal description
For any real number $a \geq 0$, the preimage of the closed interval $(-\infty, a]$ under the natural number embedding $\mathbb{N} \to \mathbb{R}$ is equal to the closed interval $(-\infty, \lfloor a \rfloor]$ in $\mathbb{N}$, where $\lfloor a \rfloor$ denotes the floor of $a$ (the greatest natural number less than or equal to $a$).
Nat.floor_add_natCast theorem
[IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) : ⌊a + n⌋₊ = ⌊a⌋₊ + n
Full source 
theorem floor_add_natCast [IsStrictOrderedRing R] (ha : 0 ≤ a) (n : ℕ) : ⌊a + n⌋₊ = ⌊a⌋₊ + n :=
  eq_of_forall_le_iff fun b => by
    rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
    obtain hb | hb := le_total n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
      refine iff_of_true ?_ le_self_add
      exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg
Floor of Sum with Natural Number: $\lfloor a + n \rfloor = \lfloor a \rfloor + n$
Informal description
Let $R$ be a strictly ordered ring and let $a \in R$ with $a \geq 0$. For any natural number $n$, the floor of $a + n$ is equal to the floor of $a$ plus $n$, i.e., $\lfloor a + n \rfloor = \lfloor a \rfloor + n$.
Nat.floor_add_one theorem
(ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1
Full source 
theorem floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1 := by
  rw [← cast_one, floor_add_natCast ha 1]
Floor of Sum with One: $\lfloor a + 1 \rfloor = \lfloor a \rfloor + 1$
Informal description
For any real number $a \geq 0$, the floor of $a + 1$ equals the floor of $a$ plus $1$, i.e., $\lfloor a + 1 \rfloor = \lfloor a \rfloor + 1$.
Nat.floor_add_ofNat theorem
(ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] : ⌊a + ofNat(n)⌋₊ = ⌊a⌋₊ + ofNat(n)
Full source 
theorem floor_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
    ⌊a + ofNat(n)⌋₊ = ⌊a⌋₊ + ofNat(n) :=
  floor_add_natCast ha n
Floor of Sum with Natural Number $\geq 2$: $\lfloor a + n \rfloor = \lfloor a \rfloor + n$
Informal description
For any real number $a \geq 0$ and any natural number $n \geq 2$, the floor of $a + n$ is equal to the floor of $a$ plus $n$, i.e., $\lfloor a + n \rfloor = \lfloor a \rfloor + n$.
Nat.floor_sub_natCast theorem
[Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) : ⌊a - n⌋₊ = ⌊a⌋₊ - n
Full source 
@[simp]
theorem floor_sub_natCast [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) :
    ⌊a - n⌋₊ = ⌊a⌋₊ - n := by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
  rcases le_total a n with h | h
  · rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
    exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)
  · rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le h)
Floor of Difference with Natural Number: $\lfloor a - n \rfloor = \lfloor a \rfloor - n$
Informal description
Let $R$ be a ring with subtraction and ordered subtraction properties, and where for any two elements $x \leq y$ there exists an element $z$ such that $x + z = y$. For any element $a \in R$ and natural number $n$, the floor of $a - n$ is equal to the floor of $a$ minus $n$, i.e., $\lfloor a - n \rfloor = \lfloor a \rfloor - n$.
Nat.floor_sub_one theorem
[Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1
Full source 
@[simp]
theorem floor_sub_one [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1 :=
  mod_cast floor_sub_natCast a 1
Floor of Difference with One: $\lfloor a - 1 \rfloor = \lfloor a \rfloor - 1$
Informal description
Let $R$ be a ring with subtraction and ordered subtraction properties, and where for any two elements $x \leq y$ there exists an element $z$ such that $x + z = y$. For any element $a \in R$, the floor of $a - 1$ is equal to the floor of $a$ minus $1$, i.e., $\lfloor a - 1 \rfloor = \lfloor a \rfloor - 1$.
Nat.floor_sub_ofNat theorem
[Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a - ofNat(n)⌋₊ = ⌊a⌋₊ - ofNat(n)
Full source 
@[simp]
theorem floor_sub_ofNat [Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌊a - ofNat(n)⌋₊ = ⌊a⌋₊ - ofNat(n) :=
  floor_sub_natCast a n
Floor of Difference with Natural Number (n ≥ 2): $\lfloor a - n \rfloor = \lfloor a \rfloor - n$
Informal description
Let $R$ be a ring with subtraction and ordered subtraction properties, and where for any two elements $x \leq y$ there exists an element $z$ such that $x + z = y$. For any element $a \in R$ and natural number $n \geq 2$, the floor of $a - n$ is equal to the floor of $a$ minus $n$, i.e., $\lfloor a - n \rfloor = \lfloor a \rfloor - n$.
Nat.ceil_add_natCast theorem
(ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n
Full source 
theorem ceil_add_natCast (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
  eq_of_forall_ge_iff fun b => by
    rw [← not_lt, ← not_lt, not_iff_not, lt_ceil]
    obtain hb | hb := le_or_lt n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)
Ceiling of Sum with Natural Number
Informal description
For any real number $a \geq 0$ and any natural number $n$, the ceiling of $a + n$ equals the ceiling of $a$ plus $n$, i.e., $\lceil a + n \rceil = \lceil a \rceil + n$.
Nat.ceil_add_one theorem
(ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1
Full source 
theorem ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1 := by
  rw [cast_one.symm, ceil_add_natCast ha 1]
Ceiling of Sum with One: $\lceil a + 1 \rceil = \lceil a \rceil + 1$
Informal description
For any real number $a \geq 0$, the ceiling of $a + 1$ equals the ceiling of $a$ plus $1$, i.e., $\lceil a + 1 \rceil = \lceil a \rceil + 1$.
Nat.ceil_add_ofNat theorem
(ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] : ⌈a + ofNat(n)⌉₊ = ⌈a⌉₊ + ofNat(n)
Full source 
theorem ceil_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
    ⌈a + ofNat(n)⌉₊ = ⌈a⌉₊ + ofNat(n) :=
  ceil_add_natCast ha n
Ceiling of Sum with Natural Number $\geq 2$: $\lceil a + n \rceil = \lceil a \rceil + n$
Informal description
For any real number $a \geq 0$ and any natural number $n \geq 2$, the ceiling of $a + n$ equals the ceiling of $a$ plus $n$, i.e., $\lceil a + n \rceil = \lceil a \rceil + n$.
Nat.ceil_lt_add_one theorem
(ha : 0 ≤ a) : (⌈a⌉₊ : R) < a + 1
Full source 
@[bound]
theorem ceil_lt_add_one (ha : 0 ≤ a) : (⌈a⌉₊ : R) < a + 1 :=
  lt_ceil.1 <| (Nat.lt_succ_self _).trans_le (ceil_add_one ha).ge
Ceiling Upper Bound: $\lceil a \rceil < a + 1$
Informal description
For any real number $a \geq 0$, the ceiling of $a$ (as a natural number) is strictly less than $a + 1$, i.e., $\lceil a \rceil < a + 1$.
Nat.ceil_add_le theorem
(a b : R) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
Full source 
@[bound]
theorem ceil_add_le (a b : R) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊ := by
  rw [ceil_le, Nat.cast_add]
  gcongr <;> apply le_ceil
Subadditivity of Ceiling Function: $\lceil a + b \rceil \leq \lceil a \rceil + \lceil b \rceil$
Informal description
For any real numbers $a$ and $b$, the ceiling of their sum is less than or equal to the sum of their individual ceilings, i.e., $\lceil a + b \rceil \leq \lceil a \rceil + \lceil b \rceil$.
Nat.sub_one_lt_floor theorem
(a : R) : a - 1 < ⌊a⌋₊
Full source 
@[bound]
theorem sub_one_lt_floor (a : R) : a - 1 < ⌊a⌋₊ :=
  sub_lt_iff_lt_add.2 <| lt_floor_add_one a
Lower bound via floor: $a - 1 < \lfloor a \rfloor$
Informal description
For any real number $a \geq 0$ in a linearly ordered semiring $R$, the value $a - 1$ is strictly less than its natural floor, i.e., $a - 1 < \lfloor a \rfloor$.
Nat.floor_div_natCast theorem
(a : K) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n
Full source 
theorem floor_div_natCast (a : K) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
  rcases le_total a 0 with ha | ha
  · rw [floor_of_nonpos, floor_of_nonpos ha]
    · simp
    apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
  obtain rfl | hn := n.eq_zero_or_pos
  · rw [cast_zero, div_zero, Nat.div_zero, floor_zero]
  refine (floor_eq_iff ?_).2 ?_
  · exact div_nonneg ha n.cast_nonneg
  constructor
  · exact cast_div_le.trans (div_le_div_of_nonneg_right (floor_le ha) n.cast_nonneg)
  rw [div_lt_iff₀, add_mul, one_mul, ← cast_mul, ← cast_add, ← floor_lt ha]
  · exact lt_div_mul_add hn
  · exact cast_pos.2 hn
Floor of Division by Natural Number: $\lfloor a / n \rfloor = \lfloor a \rfloor / n$
Informal description
For any element $a$ in a linearly ordered semiring $K$ and any natural number $n$, the floor of the division $a / n$ is equal to the floor of $a$ divided by $n$, i.e., $\lfloor a / n \rfloor = \lfloor a \rfloor / n$.
Nat.floor_div_ofNat theorem
(a : K) (n : ℕ) [n.AtLeastTwo] : ⌊a / ofNat(n)⌋₊ = ⌊a⌋₊ / ofNat(n)
Full source 
theorem floor_div_ofNat (a : K) (n : ℕ) [n.AtLeastTwo] :
    ⌊a / ofNat(n)⌋₊ = ⌊a⌋₊ / ofNat(n) :=
  floor_div_natCast a n
Floor of Division by Natural Number ≥ 2: $\lfloor a / n \rfloor = \lfloor a \rfloor / n$
Informal description
For any element $a$ in a linearly ordered semiring $K$ and any natural number $n \geq 2$, the floor of the division $a / n$ is equal to the floor of $a$ divided by $n$, i.e., $\lfloor a / n \rfloor = \lfloor a \rfloor / n$.
Nat.floor_div_eq_div theorem
(m n : ℕ) : ⌊(m : K) / n⌋₊ = m / n
Full source 
/-- Natural division is the floor of field division. -/
theorem floor_div_eq_div (m n : ℕ) : ⌊(m : K) / n⌋₊ = m / n := by
  convert floor_div_natCast (m : K) n
  rw [m.floor_natCast]
Floor of Natural Division: $\lfloor m / n \rfloor = m / n$
Informal description
For any natural numbers $m$ and $n$, and any linearly ordered semiring $K$, the floor of the division of $m$ (viewed as an element of $K$) by $n$ is equal to the natural number division of $m$ by $n$, i.e., $\lfloor m / n \rfloor = m / n$.
Nat.mul_lt_floor theorem
(hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊
Full source 
lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊ := by
  calc
    b * a < b * (⌊a⌋₊ + 1) := by gcongr; exacts [hb₀, lt_floor_add_one _]
    _ ≤ ⌊a⌋₊ := by
      rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le]
      exact le_floor hba
Product Inequality via Floor: $b \cdot a < \lfloor a \rfloor$ under $0 < b < 1$ and $\lceil \frac{b}{1-b} \rceil \leq a$
Informal description
Let $a$ and $b$ be real numbers with $0 < b < 1$. If $\lceil \frac{b}{1 - b} \rceil \leq a$, then $b \cdot a < \lfloor a \rfloor$.
Nat.ceil_lt_mul theorem
(hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉₊ < b * a
Full source 
lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉₊ < b * a := by
  obtain hab | hba := le_total a (b - 1)⁻¹
  · calc
      ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr; positivity
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]
Ceiling Upper Bound under Multiplicative Condition: $\lceil a \rceil < b \cdot a$ when $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} < a$
Informal description
For any real numbers $a$ and $b$ with $b > 1$, if $\frac{\lceil (b - 1)^{-1} \rceil}{b} < a$, then $\lceil a \rceil < b \cdot a$.
Nat.ceil_le_mul theorem
(hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b ≤ a) : ⌈a⌉₊ ≤ b * a
Full source 
lemma ceil_le_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b ≤ a) : ⌈a⌉₊ ≤ b * a := by
  obtain rfl | hba := hba.eq_or_lt
  · rw [mul_div_cancel₀, cast_le, ceil_le]
    · exact _root_.div_le_self (by positivity) hb.le
    · positivity
  · exact (ceil_lt_mul hb hba).le
Ceiling Upper Bound under Multiplicative Condition: $\lceil a \rceil \leq b \cdot a$ when $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} \leq a$
Informal description
For any real numbers $a$ and $b$ with $b > 1$, if $\frac{\lceil (b - 1)^{-1} \rceil}{b} \leq a$, then $\lceil a \rceil \leq b \cdot a$.
Nat.div_two_lt_floor theorem
(ha : 1 ≤ a) : a / 2 < ⌊a⌋₊
Full source 
lemma div_two_lt_floor (ha : 1 ≤ a) : a / 2 < ⌊a⌋₊ := by
  rw [div_eq_inv_mul]; refine mul_lt_floor ?_ ?_ ?_ <;> norm_num; assumption
Floor Lower Bound: $\lfloor a \rfloor > a/2$ for $a \geq 1$
Informal description
For any real number $a \geq 1$, the floor of $a$ is strictly greater than half of $a$, i.e., $\lfloor a \rfloor > a/2$.
Nat.ceil_lt_two_mul theorem
(ha : 2⁻¹ < a) : ⌈a⌉₊ < 2 * a
Full source 
lemma ceil_lt_two_mul (ha : 2⁻¹ < a) : ⌈a⌉₊ < 2 * a :=
  ceil_lt_mul one_lt_two (by norm_num at ha ⊢; exact ha)
Ceiling Bound for $a > 1/2$: $\lceil a \rceil < 2a$
Informal description
For any real number $a$ such that $1/2 < a$, the ceiling of $a$ is strictly less than twice $a$, i.e., $\lceil a \rceil < 2a$.
Nat.ceil_le_two_mul theorem
(ha : 2⁻¹ ≤ a) : ⌈a⌉₊ ≤ 2 * a
Full source 
lemma ceil_le_two_mul (ha : 2⁻¹ ≤ a) : ⌈a⌉₊ ≤ 2 * a :=
  ceil_le_mul one_lt_two (by norm_num at ha ⊢; exact ha)
Ceiling Upper Bound: $\lceil a \rceil \leq 2a$ for $a \geq \frac{1}{2}$
Informal description
For any real number $a$ such that $2^{-1} \leq a$, the ceiling of $a$ is less than or equal to twice $a$, i.e., $\lceil a \rceil \leq 2a$.
Nat.floor_congr theorem
[IsStrictOrderedRing R] [IsStrictOrderedRing S] (h : ∀ n : ℕ, (n : R) ≤ a ↔ (n : S) ≤ b) : ⌊a⌋₊ = ⌊b⌋₊
Full source 
theorem floor_congr [IsStrictOrderedRing R] [IsStrictOrderedRing S]
    (h : ∀ n : ℕ, (n : R) ≤ a ↔ (n : S) ≤ b) : ⌊a⌋₊ = ⌊b⌋₊ := by
  have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
  obtain ha | ha := lt_or_le a 0
  · rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_le <| h₀.not.mp ha.not_le)]
  exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)
Floor Equality under Equivalent Lower Bounds in Strictly Ordered Rings
Informal description
Let $R$ and $S$ be strictly ordered rings. For any elements $a \in R$ and $b \in S$, if for every natural number $n$ the inequality $n \leq a$ holds in $R$ if and only if $n \leq b$ holds in $S$, then the floor of $a$ equals the floor of $b$, i.e., $\lfloor a \rfloor = \lfloor b \rfloor$.
Nat.ceil_congr theorem
(h : ∀ n : ℕ, a ≤ n ↔ b ≤ n) : ⌈a⌉₊ = ⌈b⌉₊
Full source 
theorem ceil_congr (h : ∀ n : ℕ, a ≤ n ↔ b ≤ n) : ⌈a⌉₊ = ⌈b⌉₊ :=
  (ceil_le.2 <| (h _).2 <| le_ceil _).antisymm <| ceil_le.2 <| (h _).1 <| le_ceil _
Ceiling Equality under Equivalent Upper Bounds
Informal description
For any real numbers $a$ and $b$, if for every natural number $n$ the inequality $a \leq n$ holds if and only if $b \leq n$ holds, then the ceiling of $a$ equals the ceiling of $b$, i.e., $\lceil a \rceil = \lceil b \rceil$.
Nat.map_floor theorem
[IsStrictOrderedRing R] [IsStrictOrderedRing S] (f : F) (hf : StrictMono f) (a : R) : ⌊f a⌋₊ = ⌊a⌋₊
Full source 
theorem map_floor [IsStrictOrderedRing R] [IsStrictOrderedRing S]
    (f : F) (hf : StrictMono f) (a : R) : ⌊f a⌋₊ = ⌊a⌋₊ :=
  floor_congr fun n => by rw [← map_natCast f, hf.le_iff_le]
Floor Preservation under Strictly Monotone Maps between Ordered Rings
Informal description
Let $R$ and $S$ be strictly ordered rings, and let $f : R \to S$ be a strictly monotone function. For any element $a \in R$, the floor of $f(a)$ in the natural numbers equals the floor of $a$ in the natural numbers, i.e., $\lfloor f(a) \rfloor = \lfloor a \rfloor$.
Nat.map_ceil theorem
(f : F) (hf : StrictMono f) (a : R) : ⌈f a⌉₊ = ⌈a⌉₊
Full source 
theorem map_ceil (f : F) (hf : StrictMono f) (a : R) : ⌈f a⌉₊ = ⌈a⌉₊ :=
  ceil_congr fun n => by rw [← map_natCast f, hf.le_iff_le]
Ceiling Preservation under Strictly Monotone Maps between Ordered Rings
Informal description
Let $R$ and $S$ be strictly ordered rings, and let $f : R \to S$ be a strictly monotone function. For any $a \in R$, the ceiling of $f(a)$ in the natural numbers equals the ceiling of $a$ in the natural numbers, i.e., $\lceil f(a) \rceil = \lceil a \rceil$.
subsingleton_floorSemiring theorem
{R} [Semiring R] [LinearOrder R] : Subsingleton (FloorSemiring R)
Full source 
/-- There exists at most one `FloorSemiring` structure on a linear ordered semiring. -/
theorem subsingleton_floorSemiring {R} [Semiring R] [LinearOrder R] :
    Subsingleton (FloorSemiring R) := by
  refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
  have : H₁.floor = H₂.floor := by
    ext a
    rcases lt_or_le a 0 with h | h
    · rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
    · refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h
  cases H₁
  cases H₂
  congr
Uniqueness of FloorSemiring Structure on Linearly Ordered Semirings
Informal description
For any semiring $R$ with a linear order, there exists at most one `FloorSemiring` structure on $R$.