Mathlib.Algebra.Order.Floor.Ring

Int.floor_le_iff theorem

: ⌊a⌋ ≤ z ↔ a < z + 1

Full source

theorem floor_le_iff : ⌊a⌋⌊a⌋ ≤ z ↔ a < z + 1 := by rw [← lt_add_one_iff, floor_lt]; norm_cast

Floor Inequality Characterization: $\lfloor a \rfloor \leq z \leftrightarrow a < z + 1$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any integer $z$, the floor of $a$ is less than or equal to $z$ if and only if $a$ is strictly less than $z + 1$ (where $z + 1$ is viewed in $\alpha$ via the canonical embedding). In other words, $\lfloor a \rfloor \leq z \leftrightarrow a < z + 1$.

Int.lt_floor_iff theorem

: z < ⌊a⌋ ↔ z + 1 ≤ a

Full source

theorem lt_floor_iff : z < ⌊a⌋ ↔ z + 1 ≤ a := by rw [← add_one_le_iff, le_floor]; norm_cast

Characterization of Strictly Below Floor: $z < \lfloor a \rfloor \leftrightarrow z + 1 \leq a$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $\alpha$, the inequality $z < \lfloor a \rfloor$ holds if and only if $z + 1 \leq a$.

Int.floor_le_sub_one_iff theorem

: ⌊a⌋ ≤ z - 1 ↔ a < z

Full source

@[simp]
theorem floor_le_sub_one_iff : ⌊a⌋⌊a⌋ ≤ z - 1 ↔ a < z := by rw [← floor_lt, le_sub_one_iff]

Floor Inequality: $\lfloor a \rfloor \leq z - 1 \leftrightarrow a < z$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any integer $z$, the floor of $a$ is less than or equal to $z - 1$ if and only if $a$ is strictly less than $z$. In other words, $\lfloor a \rfloor \leq z - 1 \leftrightarrow a < z$.

Int.floor_le_neg_one_iff theorem

: ⌊a⌋ ≤ -1 ↔ a < 0

Full source

@[simp]
theorem floor_le_neg_one_iff : ⌊a⌋⌊a⌋ ≤ -1 ↔ a < 0 := by
  rw [← zero_sub (1 : ℤ), floor_le_sub_one_iff, cast_zero]

Floor Inequality: $\lfloor a \rfloor \leq -1 \leftrightarrow a < 0$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the floor of $a$ is less than or equal to $-1$ if and only if $a$ is strictly less than $0$, i.e., $\lfloor a \rfloor \leq -1 \leftrightarrow a < 0$.

Int.lt_succ_floor theorem

(a : R) : a < ⌊a⌋.succ

Full source

theorem lt_succ_floor (a : R) : a < ⌊a⌋.succ :=
  floor_lt.1 <| Int.lt_succ_self _

Element is Less Than Successor of Its Floor: $a < \lfloor a \rfloor + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, $a$ is strictly less than the successor of its floor, i.e., $a < \lfloor a \rfloor + 1$.

Int.lt_floor_add_one theorem

(a : R) : a < ⌊a⌋ + 1

Full source

@[simp, bound]
theorem lt_floor_add_one (a : R) : a < ⌊a⌋ + 1 := by
  simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a

Element is Less Than One Plus Its Floor: $a < \lfloor a \rfloor + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, $a$ is strictly less than $\lfloor a \rfloor + 1$.

Int.floor_mono theorem

: Monotone (floor : R → ℤ)

Full source

@[mono]
theorem floor_mono : Monotone (floor : R → ℤ) :=
  gc_coe_floor.monotone_u

Monotonicity of the Floor Function

Informal description

The floor function $\lfloor \cdot \rfloor : R \to \mathbb{Z}$ is monotone. That is, for any elements $a, b \in R$, if $a \leq b$, then $\lfloor a \rfloor \leq \lfloor b \rfloor$.

Int.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 the Floor Function: $\lfloor a \rfloor \leq \lfloor b \rfloor$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, if $a \leq b$, then the floor of $a$ is less than or equal to the floor of $b$, i.e., $\lfloor a \rfloor \leq \lfloor b \rfloor$.

Int.floor_pos theorem

: 0 < ⌊a⌋ ↔ 1 ≤ a

Full source

theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a := by
  rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]

Positivity of Floor Function: $0 < \lfloor a \rfloor \leftrightarrow 1 \leq a$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the floor of $a$ is positive if and only if $a$ is greater than or equal to $1$. That is, $0 < \lfloor a \rfloor \leftrightarrow 1 \leq a$.

Int.floor_eq_iff theorem

: ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < z + 1

Full source

theorem floor_eq_iff : ⌊a⌋⌊a⌋ = z ↔ ↑z ≤ a ∧ a < z + 1 := by
  rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]

Characterization of Floor Function: $\lfloor a \rfloor = z \leftrightarrow z \leq a < z + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function and any integer $z$, the floor of $a$ equals $z$ if and only if the canonical embedding of $z$ into $R$ satisfies $z \leq a$ and $a < z + 1$. In other words, $\lfloor a \rfloor = z \leftrightarrow z \leq a < z + 1$.

Int.floor_eq_zero_iff theorem

: ⌊a⌋ = 0 ↔ a ∈ Ico (0 : R) 1

Full source

@[simp]
theorem floor_eq_zero_iff : ⌊a⌋⌊a⌋ = 0 ↔ a ∈ Ico (0 : R) 1 := by simp [floor_eq_iff]

Floor Equals Zero iff Element in Unit Interval

Informal description

For an element $a$ in a linearly ordered ring $R$ with a floor function, the floor of $a$ equals zero if and only if $a$ belongs to the interval $[0, 1)$. In other words, $\lfloor a \rfloor = 0 \leftrightarrow a \in [0, 1)$.

Int.floor_eq_on_Ico theorem

(n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), ⌊a⌋ = n

Full source

theorem floor_eq_on_Ico (n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), ⌊a⌋ = n := fun _ ⟨h₀, h₁⟩ =>
  floor_eq_iff.mpr ⟨h₀, h₁⟩

Floor Function is Constant on Unit Intervals: $\lfloor a \rfloor = n$ for $a \in [n, n+1)$

Informal description

For any integer $n$ and any element $a$ in the interval $[n, n+1)$ of a linearly ordered ring $R$ with a floor function, the floor of $a$ equals $n$, i.e., $\lfloor a \rfloor = n$.

Int.floor_eq_on_Ico' theorem

(n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), (⌊a⌋ : R) = n

Full source

theorem floor_eq_on_Ico' (n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), (⌊a⌋ : R) = n := fun a ha =>
  congr_arg _ <| floor_eq_on_Ico n a ha

Floor Function is Constant on Unit Intervals (Coe Version): $\lfloor a \rfloor = n$ in $R$ for $a \in [n, n+1)$

Informal description

For any integer $n$ and any element $a$ in the interval $[n, n+1)$ of a linearly ordered ring $R$ with a floor function, the floor of $a$ (when viewed as an element of $R$) equals $n$, i.e., $\lfloor a \rfloor = n$ where the equality is in $R$.

Int.preimage_floor_singleton theorem

(m : ℤ) : (floor : R → ℤ) ⁻¹' { m } = Ico (m : R) (m + 1)

Full source

@[simp]
theorem preimage_floor_singleton (m : ℤ) : (floor : R → ℤ) ⁻¹' {m} = Ico (m : R) (m + 1) :=
  ext fun _ => floor_eq_iff

Preimage Characterization of Floor Function: $\lfloor \cdot \rfloor^{-1}\{m\} = [m, m+1)$

Informal description

For any integer $m$ in a linearly ordered ring $R$ with a floor function, the preimage of the singleton set $\{m\}$ under the floor function $\lfloor \cdot \rfloor : R \to \mathbb{Z}$ is equal to the left-closed right-open interval $[m, m + 1)$. In other words, $\lfloor a \rfloor = m$ if and only if $a \in [m, m + 1)$.

Int.sub_one_lt_floor theorem

(a : R) : a - 1 < ⌊a⌋

Full source

@[simp, bound]
theorem sub_one_lt_floor (a : R) : a - 1 < ⌊a⌋ :=
  sub_lt_iff_lt_add.2 (lt_floor_add_one a)

Floor Lower Bound: $a - 1 < \lfloor a \rfloor$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, we have $a - 1 < \lfloor a \rfloor$.

Int.floor_intCast theorem

(z : ℤ) : ⌊(z : R)⌋ = z

Full source

@[simp]
theorem floor_intCast (z : ℤ) : ⌊(z : R)⌋ = z :=
  eq_of_forall_le_iff fun a => by rw [le_floor, Int.cast_le]

Floor of Integer Cast: $\lfloor z \rfloor = z$

Informal description

For any integer $z$ in a linearly ordered ring $R$ with a floor function, the floor of the canonical embedding of $z$ into $R$ is equal to $z$ itself, i.e., $\lfloor z \rfloor = z$.

Int.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, ← cast_natCast, cast_le]

Floor of Natural Number Cast Equals Itself

Informal description

For any natural number $n$ and any linearly ordered ring $R$ with a floor function, the floor of the canonical embedding of $n$ into $R$ equals $n$ itself, i.e., $\lfloor n \rfloor = n$.

Int.floor_zero theorem

: ⌊(0 : R)⌋ = 0

Full source

@[simp]
theorem floor_zero : ⌊(0 : R)⌋ = 0 := by rw [← cast_zero, floor_intCast]

Floor of Zero: $\lfloor 0 \rfloor = 0$

Informal description

For any linearly ordered ring $R$ with a floor function, the floor of the zero element is zero, i.e., $\lfloor 0 \rfloor = 0$.

Int.floor_one theorem

: ⌊(1 : R)⌋ = 1

Full source

@[simp]
theorem floor_one : ⌊(1 : R)⌋ = 1 := by rw [← cast_one, floor_intCast]

Floor of One: $\lfloor 1 \rfloor = 1$

Informal description

For any linearly ordered ring $R$ with a floor function, the floor of the multiplicative identity element is one, i.e., $\lfloor 1 \rfloor = 1$.

Int.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) :=
  floor_natCast n

Floor of Natural Number ≥ 2 Equals Itself: $\lfloor n \rfloor = n$

Informal description

For any natural number $n \geq 2$ and any linearly ordered ring $R$ with a floor function, the floor of the canonical embedding of $n$ into $R$ equals $n$ itself, i.e., $\lfloor n \rfloor = n$.

Int.floor_add_intCast theorem

(a : R) (z : ℤ) : ⌊a + z⌋ = ⌊a⌋ + z

Full source

@[simp]
theorem floor_add_intCast (a : R) (z : ℤ) : ⌊a + z⌋ = ⌊a⌋ + z :=
  eq_of_forall_le_iff fun a => by
    rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]

Floor Function Additivity with Integer Shift: $\lfloor a + z \rfloor = \lfloor a \rfloor + z$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $z$, the floor of $a + z$ equals the floor of $a$ plus $z$, i.e., $\lfloor a + z \rfloor = \lfloor a \rfloor + z$.

Int.floor_add_one theorem

(a : R) : ⌊a + 1⌋ = ⌊a⌋ + 1

Full source

@[simp]
theorem floor_add_one (a : R) : ⌊a + 1⌋ = ⌊a⌋ + 1 := by
  rw [← cast_one, floor_add_intCast]

Floor Function Additivity with Unit Shift: $\lfloor a + 1 \rfloor = \lfloor a \rfloor + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the floor of $a + 1$ equals the floor of $a$ plus $1$, i.e., $\lfloor a + 1 \rfloor = \lfloor a \rfloor + 1$.

Int.le_floor_add theorem

(a b : R) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Full source

@[bound]
theorem le_floor_add (a b : R) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋ := by
  rw [le_floor, Int.cast_add]
  gcongr <;> apply floor_le

Subadditivity of the Floor Function: $\lfloor a \rfloor + \lfloor b \rfloor \leq \lfloor a + b \rfloor$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$ with a floor function, the sum of their floor values is less than or equal to the floor of their sum, i.e., $\lfloor a \rfloor + \lfloor b \rfloor \leq \lfloor a + b \rfloor$.

Int.le_floor_add_floor theorem

(a b : R) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Full source

@[bound]
theorem le_floor_add_floor (a b : R) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋ := by
  rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
  refine le_trans ?_ (sub_one_lt_floor _).le
  rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
  exact floor_le _

Near-Subadditivity of Floor Function: $\lfloor a + b \rfloor - 1 \leq \lfloor a \rfloor + \lfloor b \rfloor$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$ with a floor function, the floor of their sum minus one is less than or equal to the sum of their floors, i.e., $\lfloor a + b \rfloor - 1 \leq \lfloor a \rfloor + \lfloor b \rfloor$.

Int.floor_intCast_add theorem

(z : ℤ) (a : R) : ⌊↑z + a⌋ = z + ⌊a⌋

Full source

@[simp]
theorem floor_intCast_add (z : ℤ) (a : R) : ⌊↑z + a⌋ = z + ⌊a⌋ := by
  simpa only [add_comm] using floor_add_intCast a z

Floor Function Additivity with Integer Shift: $\lfloor z + a \rfloor = z + \lfloor a \rfloor$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $R$, the floor of $z + a$ equals $z$ plus the floor of $a$, i.e., $\lfloor z + a \rfloor = z + \lfloor a \rfloor$.

Int.floor_add_natCast theorem

(a : R) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n

Full source

@[simp]
theorem floor_add_natCast (a : R) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := by
  rw [← Int.cast_natCast, floor_add_intCast]

Floor Function Additivity with Natural Number Shift: $\lfloor a + n \rfloor = \lfloor a \rfloor + n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n$, the floor of $a + n$ equals the floor of $a$ plus $n$, i.e., $\lfloor a + n \rfloor = \lfloor a \rfloor + n$.

Int.floor_add_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n)

Full source

@[simp]
theorem floor_add_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌊a + ofNat(n)⌋ = ⌊a⌋ + ofNat(n) :=
  floor_add_natCast a n

Floor Function Additivity with Natural Number Shift (n ≥ 2): $\lfloor a + n \rfloor = \lfloor a \rfloor + n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n \geq 2$, the floor of $a + n$ equals the floor of $a$ plus $n$, i.e., $\lfloor a + n \rfloor = \lfloor a \rfloor + n$.

Int.floor_natCast_add theorem

(n : ℕ) (a : R) : ⌊↑n + a⌋ = n + ⌊a⌋

Full source

@[simp]
theorem floor_natCast_add (n : ℕ) (a : R) : ⌊↑n + a⌋ = n + ⌊a⌋ := by
  rw [← Int.cast_natCast, floor_intCast_add]

Floor Function Additivity with Natural Number Shift: $\lfloor n + a \rfloor = n + \lfloor a \rfloor$

Informal description

For any natural number $n$ and any element $a$ in a linearly ordered ring $R$, the floor of $n + a$ equals $n$ plus the floor of $a$, i.e., $\lfloor n + a \rfloor = n + \lfloor a \rfloor$.

Int.floor_ofNat_add theorem

(n : ℕ) [n.AtLeastTwo] (a : R) : ⌊ofNat(n) + a⌋ = ofNat(n) + ⌊a⌋

Full source

@[simp]
theorem floor_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : R) :
    ⌊ofNat(n) + a⌋ = ofNat(n) + ⌊a⌋ :=
  floor_natCast_add n a

Floor Function Additivity with Natural Number Shift (n ≥ 2): $\lfloor n + a \rfloor = n + \lfloor a \rfloor$

Informal description

For any natural number $n \geq 2$ and any element $a$ in a linearly ordered ring $R$, the floor of $n + a$ equals $n$ plus the floor of $a$, i.e., $\lfloor n + a \rfloor = n + \lfloor a \rfloor$.

Int.floor_sub_intCast theorem

(a : R) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z

Full source

@[simp]
theorem floor_sub_intCast (a : R) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
  Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (floor_add_intCast _ _)

Floor Function Additivity with Integer Subtraction: $\lfloor a - z \rfloor = \lfloor a \rfloor - z$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $z$, the floor of $a - z$ equals the floor of $a$ minus $z$, i.e., $\lfloor a - z \rfloor = \lfloor a \rfloor - z$.

Int.floor_sub_natCast theorem

(a : R) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n

Full source

@[simp]
theorem floor_sub_natCast (a : R) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := by
  rw [← Int.cast_natCast, floor_sub_intCast]

Floor Function Additivity with Natural Number Subtraction: $\lfloor a - n \rfloor = \lfloor a \rfloor - n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n$, the floor of $a - n$ equals the floor of $a$ minus $n$, i.e., $\lfloor a - n \rfloor = \lfloor a \rfloor - n$.

Int.floor_sub_one theorem

(a : R) : ⌊a - 1⌋ = ⌊a⌋ - 1

Full source

@[simp] theorem floor_sub_one (a : R) : ⌊a - 1⌋ = ⌊a⌋ - 1 := mod_cast floor_sub_natCast a 1

Floor Function Additivity with One: $\lfloor a - 1 \rfloor = \lfloor a \rfloor - 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the floor of $a - 1$ equals the floor of $a$ minus $1$, i.e., $\lfloor a - 1 \rfloor = \lfloor a \rfloor - 1$.

Int.floor_sub_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : ⌊a - ofNat(n)⌋ = ⌊a⌋ - ofNat(n)

Full source

@[simp]
theorem floor_sub_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌊a - ofNat(n)⌋ = ⌊a⌋ - ofNat(n) :=
  floor_sub_natCast a n

Floor Function Additivity with Subtraction of Numerals ≥ 2: $\lfloor a - n \rfloor = \lfloor a \rfloor - n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n \geq 2$, the floor of $a - n$ equals the floor of $a$ minus $n$, i.e., $\lfloor a - n \rfloor = \lfloor a \rfloor - n$.

Int.abs_sub_lt_one_of_floor_eq_floor theorem

 {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a b : R} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1

Full source

theorem abs_sub_lt_one_of_floor_eq_floor {R : Type*}
    [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    {a b : R} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1 := by
  have : a < ⌊a⌋ + 1 := lt_floor_add_one a
  have : b < ⌊b⌋ + 1 := lt_floor_add_one b
  have : (⌊a⌋ : R) = ⌊b⌋ := Int.cast_inj.2 h
  have : (⌊a⌋ : R) ≤ a := floor_le a
  have : (⌊b⌋ : R) ≤ b := floor_le b
  exact abs_sub_lt_iff.2 ⟨by linarith, by linarith⟩

Absolute Difference Less Than One When Floors Are Equal

Informal description

Let $R$ be a commutative, linearly ordered ring with a strict order and a floor function. For any two elements $a, b \in R$ such that $\lfloor a \rfloor = \lfloor b \rfloor$, the absolute difference between $a$ and $b$ is strictly less than $1$, i.e., $|a - b| < 1$.

Int.floor_eq_self_iff_mem theorem

(a : R) : ⌊a⌋ = a ↔ a ∈ Set.range Int.cast

Full source

lemma floor_eq_self_iff_mem (a : R) : ⌊a⌋⌊a⌋ = a ↔ a ∈ Set.range Int.cast := by
  aesop

Floor Equals Identity iff Integer-Valued

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the floor of $a$ equals $a$ itself if and only if $a$ is in the range of the integer embedding into $R$, i.e., $\lfloor a \rfloor = a \leftrightarrow a \in \mathbb{Z}$ (where $\mathbb{Z}$ is viewed as a subset of $R$ via the canonical embedding).

Int.self_sub_floor theorem

(a : R) : a - ⌊a⌋ = fract a

Full source

@[simp]
theorem self_sub_floor (a : R) : a - ⌊a⌋ = fract a :=
  rfl

Difference Equals Fractional Part: $a - \lfloor a \rfloor = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the difference between $a$ and its floor $\lfloor a \rfloor$ equals the fractional part $\text{fract}(a)$, i.e., $a - \lfloor a \rfloor = \text{fract}(a)$.

Int.floor_add_fract theorem

(a : R) : (⌊a⌋ : R) + fract a = a

Full source

@[simp]
theorem floor_add_fract (a : R) : (⌊a⌋ : R) + fract a = a :=
  add_sub_cancel _ _

Decomposition of an Element into Floor and Fractional Part

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the sum of the floor of $a$ (interpreted as an element of $R$) and the fractional part of $a$ equals $a$ itself, i.e., $\lfloor a \rfloor + \text{fract}(a) = a$.

Int.fract_add_floor theorem

(a : R) : fract a + ⌊a⌋ = a

Full source

@[simp]
theorem fract_add_floor (a : R) : fract a + ⌊a⌋ = a :=
  sub_add_cancel _ _

Additive Decomposition via Floor and Fractional Part: $\text{fract}(a) + \lfloor a \rfloor = a$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the sum of the fractional part $\text{fract}(a)$ and the floor $\lfloor a \rfloor$ equals $a$, i.e., $\text{fract}(a) + \lfloor a \rfloor = a$.

Int.self_sub_fract theorem

(a : R) : a - fract a = ⌊a⌋

Full source

@[simp]
theorem self_sub_fract (a : R) : a - fract a = ⌊a⌋ :=
  sub_sub_cancel _ _

Difference of Element and Fractional Part Equals Floor

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the difference between $a$ and its fractional part equals its floor, i.e., $a - \text{fract}(a) = \lfloor a \rfloor$.

Int.fract_sub_self theorem

(a : R) : fract a - a = -⌊a⌋

Full source

@[simp]
theorem fract_sub_self (a : R) : fract a - a = -⌊a⌋ :=
  sub_sub_cancel_left _ _

Difference Between Fractional Part and Element Equals Negative Floor: $\text{fract}(a) - a = -\lfloor a \rfloor$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the difference between the fractional part $\text{fract}(a)$ and $a$ equals the negation of the floor of $a$, i.e., \[ \text{fract}(a) - a = -\lfloor a \rfloor. \]

Int.fract_add theorem

(a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z

Full source

theorem fract_add (a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
  ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by
    unfold fract
    simp only [sub_eq_add_neg, neg_add_rev, neg_neg, cast_add, cast_neg]
    abel⟩

Additivity of Fractional Parts Modulo Integers

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, there exists an integer $z$ such that the difference between the fractional part of $a + b$ and the sum of the fractional parts of $a$ and $b$ equals $z$, i.e., \[ \text{fract}(a + b) - \text{fract}(a) - \text{fract}(b) = z. \]

Int.fract_add_intCast theorem

(a : R) (m : ℤ) : fract (a + m) = fract a

Full source

@[simp]
theorem fract_add_intCast (a : R) (m : ℤ) : fract (a + m) = fract a := by
  rw [fract]
  simp

Fractional Part Invariance Under Integer Addition: $\text{fract}(a + m) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $m$, the fractional part of $a + m$ equals the fractional part of $a$, i.e., $\text{fract}(a + m) = \text{fract}(a)$.

Int.fract_add_natCast theorem

(a : R) (m : ℕ) : fract (a + m) = fract a

Full source

@[simp]
theorem fract_add_natCast (a : R) (m : ℕ) : fract (a + m) = fract a := by
  rw [fract]
  simp

Fractional Part Invariance Under Natural Number Addition: $\text{fract}(a + m) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $m$, the fractional part of $a + m$ equals the fractional part of $a$, i.e., $\text{fract}(a + m) = \text{fract}(a)$.

Int.fract_add_one theorem

(a : R) : fract (a + 1) = fract a

Full source

@[simp]
theorem fract_add_one (a : R) : fract (a + 1) = fract a := mod_cast fract_add_natCast a 1

Fractional Part Invariance Under Addition of One: $\text{fract}(a + 1) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part of $a + 1$ equals the fractional part of $a$, i.e., $\text{fract}(a + 1) = \text{fract}(a)$.

Int.fract_add_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : fract (a + ofNat(n)) = fract a

Full source

@[simp]
theorem fract_add_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    fract (a + ofNat(n)) = fract a :=
  fract_add_natCast a n

Fractional Part Invariance Under Addition of Natural Numbers ≥ 2: $\text{fract}(a + n) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n \geq 2$, the fractional part of $a + n$ equals the fractional part of $a$, i.e., $\text{fract}(a + n) = \text{fract}(a)$.

Int.fract_intCast_add theorem

(m : ℤ) (a : R) : fract (↑m + a) = fract a

Full source

@[simp]
theorem fract_intCast_add (m : ℤ) (a : R) : fract (↑m + a) = fract a := by
  rw [add_comm, fract_add_intCast]

Fractional Part Invariance Under Integer Addition: $\text{fract}(m + a) = \text{fract}(a)$

Informal description

For any integer $m$ and any element $a$ in a linearly ordered ring $R$, the fractional part of the sum $m + a$ equals the fractional part of $a$, i.e., $\text{fract}(m + a) = \text{fract}(a)$.

Int.fract_natCast_add theorem

(n : ℕ) (a : R) : fract (↑n + a) = fract a

Full source

@[simp]
theorem fract_natCast_add (n : ℕ) (a : R) : fract (↑n + a) = fract a := by
  rw [add_comm, fract_add_natCast]

Fractional Part Invariance Under Natural Number Addition: $\text{fract}(n + a) = \text{fract}(a)$

Informal description

For any natural number $n$ and any element $a$ in a linearly ordered ring $R$, the fractional part of the sum $n + a$ equals the fractional part of $a$, i.e., $\text{fract}(n + a) = \text{fract}(a)$.

Int.fract_one_add theorem

(a : R) : fract (1 + a) = fract a

Full source

@[simp]
theorem fract_one_add (a : R) : fract (1 + a) = fract a := mod_cast fract_natCast_add 1 a

Fractional Part Invariance Under Addition of One: $\text{fract}(1 + a) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part of $1 + a$ equals the fractional part of $a$, i.e., $\text{fract}(1 + a) = \text{fract}(a)$.

Int.fract_ofNat_add theorem

(n : ℕ) [n.AtLeastTwo] (a : R) : fract (ofNat(n) + a) = fract a

Full source

@[simp]
theorem fract_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : R) :
    fract (ofNat(n) + a) = fract a :=
  fract_natCast_add n a

Fractional Part Invariance Under Addition of Numerals ≥ 2: $\text{fract}(n + a) = \text{fract}(a)$

Informal description

For any natural number $n \geq 2$ and any element $a$ in a linearly ordered ring $R$, the fractional part of the sum $\text{ofNat}(n) + a$ equals the fractional part of $a$, i.e., $\text{fract}(\text{ofNat}(n) + a) = \text{fract}(a)$.

Int.fract_sub_intCast theorem

(a : R) (m : ℤ) : fract (a - m) = fract a

Full source

@[simp]
theorem fract_sub_intCast (a : R) (m : ℤ) : fract (a - m) = fract a := by
  rw [fract]
  simp

Invariance of Fractional Part under Integer Subtraction: $\text{fract}(a - m) = \text{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $m$, the fractional part of $a - m$ equals the fractional part of $a$, i.e., $\text{fract}(a - m) = \text{fract}(a)$.

Int.fract_sub_natCast theorem

(a : R) (n : ℕ) : fract (a - n) = fract a

Full source

@[simp]
theorem fract_sub_natCast (a : R) (n : ℕ) : fract (a - n) = fract a := by
  rw [fract]
  simp

Invariance of Fractional Part under Natural Number Subtraction

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n$, the fractional part of $a - n$ equals the fractional part of $a$, i.e., $\text{fract}(a - n) = \text{fract}(a)$.

Int.fract_sub_one theorem

(a : R) : fract (a - 1) = fract a

Full source

@[simp]
theorem fract_sub_one (a : R) : fract (a - 1) = fract a := mod_cast fract_sub_natCast a 1

Invariance of Fractional Part under Subtraction of One

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part of $a - 1$ equals the fractional part of $a$, i.e., $\text{fract}(a - 1) = \text{fract}(a)$.

Int.fract_sub_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : fract (a - ofNat(n)) = fract a

Full source

@[simp]
theorem fract_sub_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    fract (a - ofNat(n)) = fract a :=
  fract_sub_natCast a n

Invariance of Fractional Part under Subtraction of Natural Numbers ≥ 2

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n \geq 2$, the fractional part of $a - n$ equals the fractional part of $a$, i.e., $\text{fract}(a - n) = \text{fract}(a)$.

Int.fract_add_le theorem

(a b : R) : fract (a + b) ≤ fract a + fract b

Full source

theorem fract_add_le (a b : R) : fract (a + b) ≤ fract a + fract b := by
  rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]
  exact le_floor_add _ _

Subadditivity of the Fractional Part: $\operatorname{fract}(a + b) \leq \operatorname{fract}(a) + \operatorname{fract}(b)$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the fractional part of their sum satisfies $\operatorname{fract}(a + b) \leq \operatorname{fract}(a) + \operatorname{fract}(b)$, where $\operatorname{fract}(x) := x - \lfloor x \rfloor$ denotes the fractional part of $x$.

Int.fract_add_fract_le theorem

(a b : R) : fract a + fract b ≤ fract (a + b) + 1

Full source

theorem fract_add_fract_le (a b : R) : fract a + fract b ≤ fract (a + b) + 1 := by
  rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]
  exact mod_cast le_floor_add_floor a b

Near-Superadditivity of Fractional Parts: $\{a\} + \{b\} \leq \{a + b\} + 1$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$ with a floor function, the sum of their fractional parts satisfies $\{a\} + \{b\} \leq \{a + b\} + 1$, where $\{x\} := x - \lfloor x \rfloor$ denotes the fractional part of $x$.

Int.fract_nonneg theorem

(a : R) : 0 ≤ fract a

Full source

@[simp]
theorem fract_nonneg (a : R) : 0 ≤ fract a :=
  sub_nonneg.2 <| floor_le _

Nonnegativity of the Fractional Part

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a) := a - \lfloor a \rfloor$ is nonnegative, i.e., $0 \leq \operatorname{fract}(a)$.

Int.fract_pos theorem

: 0 < fract a ↔ a ≠ ⌊a⌋

Full source

/-- The fractional part of `a` is positive if and only if `a ≠ ⌊a⌋`. -/
lemma fract_pos : 0 < fract a ↔ a ≠ ⌊a⌋ :=
  (fract_nonneg a).lt_iff_ne.trans <| ne_comm.trans sub_ne_zero

Positivity of Fractional Part Equivalent to Non-Integer Value

Informal description

For an element $a$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a) := a - \lfloor a \rfloor$ is positive if and only if $a$ is not equal to its floor, i.e., $0 < \operatorname{fract}(a) \leftrightarrow a \neq \lfloor a \rfloor$.

Int.fract_lt_one theorem

(a : R) : fract a < 1

Full source

theorem fract_lt_one (a : R) : fract a < 1 :=
  sub_lt_comm.1 <| sub_one_lt_floor _

Upper bound on fractional part: $\operatorname{fract}(a) < 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a) := a - \lfloor a \rfloor$ satisfies $\operatorname{fract}(a) < 1$.

Int.fract_zero theorem

: fract (0 : R) = 0

Full source

@[simp]
theorem fract_zero : fract (0 : R) = 0 := by rw [fract, floor_zero, cast_zero, sub_self]

Fractional Part of Zero: $\operatorname{fract}(0) = 0$

Informal description

For any linearly ordered ring $R$ with a floor function, the fractional part of zero is zero, i.e., $\operatorname{fract}(0) = 0$.

Int.fract_one theorem

: fract (1 : R) = 0

Full source

@[simp]
theorem fract_one : fract (1 : R) = 0 := by simp [fract]

Fractional Part of One is Zero

Informal description

For any linearly ordered ring $R$ with a floor function, the fractional part of the multiplicative identity element is zero, i.e., $\operatorname{fract}(1) = 0$.

Int.abs_fract theorem

: |fract a| = fract a

Full source

theorem abs_fract : |fract a| = fract a :=
  abs_eq_self.mpr <| fract_nonneg a

Absolute Value of Fractional Part Equals Itself

Informal description

For any element $a$ in a linearly ordered ring $R$, the absolute value of the fractional part $\operatorname{fract}(a) := a - \lfloor a \rfloor$ is equal to itself, i.e., $|\operatorname{fract}(a)| = \operatorname{fract}(a)$.

Int.abs_one_sub_fract theorem

: |1 - fract a| = 1 - fract a

Full source

@[simp]
theorem abs_one_sub_fract : |1 - fract a| = 1 - fract a :=
  abs_eq_self.mpr <| sub_nonneg.mpr (fract_lt_one a).le

Absolute value identity for $1 - \operatorname{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$, the absolute value of $1 - \operatorname{fract}(a)$ equals $1 - \operatorname{fract}(a)$, i.e., $|1 - \operatorname{fract}(a)| = 1 - \operatorname{fract}(a)$.

Int.fract_intCast theorem

(z : ℤ) : fract (z : R) = 0

Full source

@[simp]
theorem fract_intCast (z : ℤ) : fract (z : R) = 0 := by
  unfold fract
  rw [floor_intCast]
  exact sub_self _

Fractional Part of Integer is Zero

Informal description

For any integer $z$ in a linearly ordered ring $R$ with a floor function, the fractional part of the canonical embedding of $z$ into $R$ is zero, i.e., $\operatorname{fract}(z) = 0$.

Int.fract_natCast theorem

(n : ℕ) : fract (n : R) = 0

Full source

@[simp]
theorem fract_natCast (n : ℕ) : fract (n : R) = 0 := by simp [fract]

Fractional Part of Natural Number Cast is Zero

Informal description

For any natural number $n$ and any linearly ordered ring $R$ with a floor function, the fractional part of the canonical embedding of $n$ into $R$ is zero, i.e., $\text{fract}(n) = 0$.

Int.fract_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : fract (ofNat(n) : R) = 0

Full source

@[simp]
theorem fract_ofNat (n : ℕ) [n.AtLeastTwo] :
    fract (ofNat(n) : R) = 0 :=
  fract_natCast n

Fractional Part of Natural Number ≥ 2 is Zero

Informal description

For any natural number $n \geq 2$ and any linearly ordered ring $R$ with a floor function, the fractional part of the canonical embedding of $n$ into $R$ is zero, i.e., $\operatorname{fract}(n) = 0$.

Int.fract_floor theorem

(a : R) : fract (⌊a⌋ : R) = 0

Full source

theorem fract_floor (a : R) : fract (⌊a⌋ : R) = 0 :=
  fract_intCast _

Fractional Part of Floor is Zero

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the fractional part of the floor of $a$ is zero, i.e., $\operatorname{fract}(\lfloor a \rfloor) = 0$.

Int.floor_fract theorem

(a : R) : ⌊fract a⌋ = 0

Full source

@[simp]
theorem floor_fract (a : R) : ⌊fract a⌋ = 0 := by
  rw [floor_eq_iff, Int.cast_zero, zero_add]; exact ⟨fract_nonneg _, fract_lt_one _⟩

Floor of Fractional Part is Zero

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the floor of the fractional part of $a$ is zero, i.e., $\lfloor \operatorname{fract}(a) \rfloor = 0$.

Int.fract_eq_iff theorem

{a b : R} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : ℤ, a - b = z

Full source

theorem fract_eq_iff {a b : R} : fractfract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : ℤ, a - b = z :=
  ⟨fun h => by
    rw [← h]
    exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩,
   by
    rintro ⟨h₀, h₁, z, hz⟩
    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz,
      Int.cast_inj, floor_eq_iff, ← hz]
    constructor <;> simpa [sub_eq_add_neg, add_assoc] ⟩

Characterization of Fractional Part: $\operatorname{fract}(a) = b \leftrightarrow 0 \leq b < 1 \land \exists z \in \mathbb{Z}, a - b = z$

Informal description

For any elements $a, b$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a) = b$ if and only if $0 \leq b < 1$ and there exists an integer $z$ such that $a - b = z$.

Int.fract_eq_fract theorem

{a b : R} : fract a = fract b ↔ ∃ z : ℤ, a - b = z

Full source

theorem fract_eq_fract {a b : R} : fractfract a = fract b ↔ ∃ z : ℤ, a - b = z :=
  ⟨fun h => ⟨⌊a⌋ - ⌊b⌋, by unfold fract at h; rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]⟩,
   by
    rintro ⟨z, hz⟩
    refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
    rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
    exact add_sub_sub_cancel _ _ _⟩

Fractional Parts Equality Criterion: $\operatorname{fract}(a) = \operatorname{fract}(b) \leftrightarrow a - b \in \mathbb{Z}$

Informal description

For any elements $a, b$ in a linearly ordered ring $R$, the fractional parts $\operatorname{fract}(a)$ and $\operatorname{fract}(b)$ are equal if and only if there exists an integer $z$ such that $a - b = z$.

Int.fract_eq_self theorem

{a : R} : fract a = a ↔ 0 ≤ a ∧ a < 1

Full source

@[simp]
theorem fract_eq_self {a : R} : fractfract a = a ↔ 0 ≤ a ∧ a < 1 :=
  fract_eq_iff.trans <| and_assoc.symm.trans <| and_iff_left ⟨0, by simp⟩

Characterization of Fixed Points of the Fractional Part Function: $\operatorname{fract}(a) = a \leftrightarrow 0 \leq a < 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a)$ equals $a$ if and only if $0 \leq a < 1$.

Int.fract_fract theorem

(a : R) : fract (fract a) = fract a

Full source

@[simp]
theorem fract_fract (a : R) : fract (fract a) = fract a :=
  fract_eq_self.2 ⟨fract_nonneg _, fract_lt_one _⟩

Idempotence of the Fractional Part Function: $\operatorname{fract}(\operatorname{fract}(a)) = \operatorname{fract}(a)$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the fractional part of the fractional part of $a$ equals the fractional part of $a$, i.e., $\operatorname{fract}(\operatorname{fract}(a)) = \operatorname{fract}(a)$.

Int.fract_neg theorem

{x : R} (hx : fract x ≠ 0) : fract (-x) = 1 - fract x

Full source

theorem fract_neg {x : R} (hx : fractfract x ≠ 0) : fract (-x) = 1 - fract x := by
  rw [fract_eq_iff]
  constructor
  · rw [le_sub_iff_add_le, zero_add]
    exact (fract_lt_one x).le
  refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩
  simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]
  conv in -x => rw [← floor_add_fract x]
  simp [-floor_add_fract]

Fractional Part of Negative Element: $\operatorname{fract}(-x) = 1 - \operatorname{fract}(x)$ when $\operatorname{fract}(x) \neq 0$

Informal description

For any element $x$ in a linearly ordered ring $R$ with a floor function, if the fractional part $\operatorname{fract}(x) \neq 0$, then the fractional part of $-x$ is given by $\operatorname{fract}(-x) = 1 - \operatorname{fract}(x)$.

Int.fract_neg_eq_zero theorem

{x : R} : fract (-x) = 0 ↔ fract x = 0

Full source

@[simp]
theorem fract_neg_eq_zero {x : R} : fractfract (-x) = 0 ↔ fract x = 0 := by
  simp only [fract_eq_iff, le_refl, zero_lt_one, tsub_zero, true_and]
  constructor <;> rintro ⟨z, hz⟩ <;> use -z <;> simp [← hz]

Fractional Part Negation Zero Criterion: $\text{fract}(-x) = 0 \leftrightarrow \text{fract}(x) = 0$

Informal description

For any element $x$ in a linearly ordered ring $R$ with a floor function, the fractional part of $-x$ is zero if and only if the fractional part of $x$ is zero, i.e., $\text{fract}(-x) = 0 \leftrightarrow \text{fract}(x) = 0$.

Int.fract_mul_natCast theorem

(a : R) (b : ℕ) : ∃ z : ℤ, fract a * b - fract (a * b) = z

Full source

theorem fract_mul_natCast (a : R) (b : ℕ) : ∃ z : ℤ, fract a * b - fract (a * b) = z := by
  induction b with
  | zero => use 0; simp
  | succ c hc =>
    rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel

Fractional Part and Natural Multiplication Relation: $\text{fract}(a) \cdot b - \text{fract}(a \cdot b) \in \mathbb{Z}$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function and any natural number $b$, there exists an integer $z$ such that the difference between the product of the fractional part of $a$ and $b$ and the fractional part of $a \cdot b$ equals $z$, i.e., \[ \text{fract}(a) \cdot b - \text{fract}(a \cdot b) = z. \]

Int.preimage_fract theorem

(s : Set R) : fract ⁻¹' s = ⋃ m : ℤ, (fun x => x - (m : R)) ⁻¹' (s ∩ Ico (0 : R) 1)

Full source

theorem preimage_fract (s : Set R) :
    fractfract ⁻¹' s = ⋃ m : ℤ, (fun x => x - (m : R)) ⁻¹' (s ∩ Ico (0 : R) 1) := by
  ext x
  simp only [mem_preimage, mem_iUnion, mem_inter_iff]
  refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
  rintro ⟨m, hms, hm0, hm1⟩
  obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
  exact hms

Preimage Characterization of Fractional Part: $\operatorname{fract}^{-1}(s) = \bigcup_{m \in \mathbb{Z}} (s \cap [0,1)) + m$

Informal description

For any subset $s$ of a linearly ordered ring $R$ with a floor function, the preimage of $s$ under the fractional part function $\operatorname{fract}$ is equal to the union over all integers $m$ of the preimages of $s \cap [0, 1)$ under the translation function $x \mapsto x - m$. In other words: \[ \operatorname{fract}^{-1}(s) = \bigcup_{m \in \mathbb{Z}} \{x \in R \mid x - m \in s \cap [0, 1)\} \]

Int.image_fract theorem

(s : Set R) : fract '' s = ⋃ m : ℤ, (fun x : R => x - m) '' s ∩ Ico 0 1

Full source

theorem image_fract (s : Set R) : fractfract '' s = ⋃ m : ℤ, (fun x : R => x - m) '' s ∩ Ico 0 1 := by
  ext x
  simp only [mem_image, mem_inter_iff, mem_iUnion]; constructor
  · rintro ⟨y, hy, rfl⟩
    exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩
  · rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩
    obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
    exact ⟨y, hys, rfl⟩

Image of Fractional Part as Union of Translated Sets Intersected with Unit Interval

Informal description

For any subset $s$ of a linearly ordered ring $R$, the image of $s$ under the fractional part function $\operatorname{fract}$ is equal to the union over all integers $m$ of the intersection between the image of $s$ under the translation $x \mapsto x - m$ and the interval $[0, 1)$. In other words, \[ \operatorname{fract}(s) = \bigcup_{m \in \mathbb{Z}} (s - m) \cap [0, 1). \]

Int.fract_div_mul_self_mem_Ico theorem

(a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Ico 0 a

Full source

theorem fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fractfract (b / a) * a ∈ Ico 0 a :=
  ⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)),
    (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩

Fractional Part of Division Scaled by Divisor Lies in $[0, a)$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $k$ with $a > 0$, the product of the fractional part of $b/a$ and $a$ lies in the interval $[0, a)$. That is, \[ \left(\frac{b}{a} - \left\lfloor \frac{b}{a} \right\rfloor\right) \cdot a \in [0, a). \]

Int.fract_div_mul_self_add_zsmul_eq theorem

(a b : k) (ha : a ≠ 0) : fract (b / a) * a + ⌊b / a⌋ • a = b

Full source

theorem fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) :
    fract (b / a) * a + ⌊b / a⌋ • a = b := by
  rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

Additive Decomposition via Floor and Fractional Part: $\text{fract}(b/a) \cdot a + \lfloor b/a \rfloor \cdot a = b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $k$ with $a \neq 0$, the sum of the fractional part of $b/a$ multiplied by $a$ and the floor of $b/a$ multiplied by $a$ equals $b$, i.e., \[ \text{fract}\left(\frac{b}{a}\right) \cdot a + \left\lfloor \frac{b}{a} \right\rfloor \cdot a = b. \]

Int.sub_floor_div_mul_nonneg theorem

(a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ * b

Full source

theorem sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ * b :=
  sub_nonneg_of_le <| (le_div_iff₀ hb).1 <| floor_le _

Nonnegativity of Remainder After Floor Division: $0 \leq a - \lfloor a/b \rfloor \cdot b$ for $b > 0$

Informal description

For any element $a$ in a linearly ordered ring $k$ and any positive element $b \in k$, the difference $a - \lfloor a / b \rfloor \cdot b$ is nonnegative, i.e., \[ 0 \leq a - \left\lfloor \frac{a}{b} \right\rfloor \cdot b. \]

Int.sub_floor_div_mul_lt theorem

(a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b

Full source

theorem sub_floor_div_mul_lt (a : k) (hb : 0 < b) : a - ⌊a / b⌋ * b < b :=
  sub_lt_iff_lt_add.2 <| by
    rw [← one_add_mul, ← div_lt_iff₀ hb, add_comm]
    exact lt_floor_add_one _

Remainder Bound After Floor Division: $a - \lfloor a/b \rfloor \cdot b < b$ for $b > 0$

Informal description

For any element $a$ in a linearly ordered ring $k$ and any positive element $b \in k$, the difference $a - \lfloor a / b \rfloor \cdot b$ is strictly less than $b$, i.e., \[ a - \left\lfloor \frac{a}{b} \right\rfloor \cdot b < b. \]

Int.fract_div_natCast_eq_div_natCast_mod theorem

{m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n

Full source

theorem fract_div_natCast_eq_div_natCast_mod {m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n := by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  have hn' : 0 < (n : k) := by
    norm_cast
  refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
  · positivity
  · simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn
  · rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']
    norm_cast
    rw [← Nat.cast_add, Nat.mod_add_div m n]

Fractional Part of Natural Number Division Equals Remainder Divided by Divisor

Informal description

For any natural numbers $m$ and $n$, and any linearly ordered ring $k$ with a floor function, the fractional part of the division $\frac{m}{n}$ in $k$ equals $\frac{m \bmod n}{n}$, i.e., \[ \operatorname{fract}\left(\frac{m}{n}\right) = \frac{m \bmod n}{n}. \]

Int.fract_div_intCast_eq_div_intCast_mod theorem

{m : ℤ} {n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n

Full source

theorem fract_div_intCast_eq_div_intCast_mod {m : ℤ} {n : ℕ} :
    fract ((m : k) / n) = ↑(m % n) / n := by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  replace hn : 0 < (n : k) := by norm_cast
  have : ∀ {l : ℤ}, 0 ≤ l → fract ((l : k) / n) = ↑(l % n) / n := by
    intros l hl
    obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
    · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
    · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]
  obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
  · exact this (ofNat_nonneg m₀)
  let q := ⌈↑m₀ / (n : k)⌉
  let m₁ := q * ↑n - (↑m₀ : ℤ)
  have hm₁ : 0 ≤ m₁ := by
    simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _
  calc
    fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
      = fract (-(m₀ : k) / n) := by simp
    _ = fract ((m₁ : k) / n) := ?_
    _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
    _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_
  · rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]
    simp [m₁]
  · congr 2
    simp only [m₁]
    rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]

Fractional Part of Integer Division Equals Remainder Divided by Divisor

Informal description

For any integer $m$ and natural number $n$, and any linearly ordered ring $k$ with a floor function, the fractional part of the division $\frac{m}{n}$ in $k$ equals $\frac{m \bmod n}{n}$, i.e., \[ \operatorname{fract}\left(\frac{m}{n}\right) = \frac{m \bmod n}{n}. \]

Int.add_one_le_ceil_iff theorem

: z + 1 ≤ ⌈a⌉ ↔ (z : R) < a

Full source

@[simp]
theorem add_one_le_ceil_iff : z + 1 ≤ ⌈a⌉ ↔ (z : R) < a := by rw [← lt_ceil, add_one_le_iff]

Characterization of Ceiling via Strict Inequality: $z + 1 \leq \lceil a \rceil \leftrightarrow z < a$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $R$, the inequality $z + 1 \leq \lceil a \rceil$ holds if and only if the canonical embedding of $z$ into $R$ is strictly less than $a$, i.e., $(z : R) < a$.

Int.one_le_ceil_iff theorem

: 1 ≤ ⌈a⌉ ↔ 0 < a

Full source

@[simp]
theorem one_le_ceil_iff : 1 ≤ ⌈a⌉ ↔ 0 < a := by
  rw [← zero_add (1 : ℤ), add_one_le_ceil_iff, cast_zero]

Ceiling Inequality: $1 \leq \lceil a \rceil \leftrightarrow 0 < a$

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling function satisfies $1 \leq \lceil a \rceil$ if and only if $0 < a$.

Int.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, Int.cast_add, Int.cast_one]
  exact (lt_floor_add_one a).le

Ceiling and Floor Inequality: $\lceil a \rceil \leq \lfloor a \rfloor + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling of $a$ is less than or equal to the floor of $a$ plus one, i.e., $\lceil a \rceil \leq \lfloor a \rfloor + 1$.

Int.le_ceil_iff theorem

: z ≤ ⌈a⌉ ↔ z - 1 < a

Full source

lemma le_ceil_iff : z ≤ ⌈a⌉ ↔ z - 1 < a := by rw [← sub_one_lt_iff, lt_ceil]; norm_cast

Characterization of Ceiling Function: $z \leq \lceil a \rceil \leftrightarrow z - 1 < a$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $R$, the inequality $z \leq \lceil a \rceil$ holds if and only if $z - 1 < a$.

Int.ceil_lt_iff theorem

: ⌈a⌉ < z ↔ a ≤ z - 1

Full source

lemma ceil_lt_iff : ⌈a⌉⌈a⌉ < z ↔ a ≤ z - 1 := by rw [← le_sub_one_iff, ceil_le]; norm_cast

Ceiling Strict Inequality: $\lceil a \rceil < z \leftrightarrow a \leq z - 1$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $z$, the ceiling of $a$ is strictly less than $z$ if and only if $a$ is less than or equal to $z - 1$.

Int.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{Z}$ is monotone, meaning that for any $a, b \in R$, if $a \leq b$ then $\lceil a \rceil \leq \lceil b \rceil$.

Int.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 the ceiling function: $a \leq b \Rightarrow \lceil a \rceil \leq \lceil b \rceil$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $\alpha$ with a floor function, if $a \leq b$, then the ceiling of $a$ is less than or equal to the ceiling of $b$, i.e., $\lceil a \rceil \leq \lceil b \rceil$.

Int.ceil_nonneg_of_neg_one_lt theorem

(ha : -1 < a) : 0 ≤ ⌈a⌉

Full source

theorem ceil_nonneg_of_neg_one_lt (ha : -1 < a) : 0 ≤ ⌈a⌉ := by
  rwa [Int.le_ceil_iff, Int.cast_zero, zero_sub]

Nonnegativity of Ceiling for Elements Greater Than Negative One

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ with a floor function, if $-1 < a$, then the ceiling of $a$ is nonnegative, i.e., $0 \leq \lceil a \rceil$.

Int.ceil_eq_iff theorem

: ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ z

Full source

theorem ceil_eq_iff : ⌈a⌉⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ z := by
  rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]

Characterization of Ceiling Equality: $\lceil a \rceil = z \leftrightarrow z - 1 < a \leq z$

Informal description

For an element $a$ in a linearly ordered ring $\alpha$ and an integer $z$, the ceiling of $a$ equals $z$ if and only if $a$ satisfies $z - 1 < a \leq z$ (where $z$ is viewed as an element of $\alpha$ via the canonical embedding).

Int.ceil_eq_zero_iff theorem

: ⌈a⌉ = 0 ↔ a ∈ Ioc (-1 : R) 0

Full source

@[simp]
theorem ceil_eq_zero_iff : ⌈a⌉⌈a⌉ = 0 ↔ a ∈ Ioc (-1 : R) 0 := by simp [ceil_eq_iff]

Characterization of Zero Ceiling: $\lceil a \rceil = 0 \leftrightarrow a \in (-1, 0]$

Informal description

For an element $a$ in a linearly ordered ring $R$, the ceiling function satisfies $\lceil a \rceil = 0$ if and only if $a$ belongs to the interval $(-1, 0]$.

Int.ceil_eq_on_Ioc theorem

(z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, ⌈a⌉ = z

Full source

theorem ceil_eq_on_Ioc (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, ⌈a⌉ = z := fun _ ⟨h₀, h₁⟩ =>
  ceil_eq_iff.mpr ⟨h₀, h₁⟩

Ceiling Function is Constant on $(z-1, z]$

Informal description

For any integer $z$ and any element $a$ in the interval $(z-1, z]$ of a linearly ordered ring $R$, the ceiling function satisfies $\lceil a \rceil = z$.

Int.preimage_ceil_singleton theorem

(m : ℤ) : (ceil : R → ℤ) ⁻¹' { m } = Ioc ((m : R) - 1) m

Full source

@[simp]
theorem preimage_ceil_singleton (m : ℤ) : (ceil : R → ℤ) ⁻¹' {m} = Ioc ((m : R) - 1) m :=
  ext fun _ => ceil_eq_iff

Preimage Characterization of Ceiling Function: $\lceil \cdot \rceil^{-1}\{m\} = (m - 1, m]$

Informal description

For any integer $m$ in a linearly ordered ring $R$, the preimage of the singleton set $\{m\}$ under the ceiling function $\lceil \cdot \rceil : R \to \mathbb{Z}$ is equal to the left-open right-closed interval $(m - 1, m]$. In other words, $\lceil a \rceil = m$ if and only if $a \in (m - 1, m]$.

Int.floor_neg theorem

: ⌊-a⌋ = -⌈a⌉

Full source

theorem floor_neg : ⌊-a⌋ = -⌈a⌉ :=
  eq_of_forall_le_iff fun z => by rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

Floor of Negative Equals Negative of Ceiling: $\lfloor -a \rfloor = -\lceil a \rceil$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the floor of $-a$ equals the negation of the ceiling of $a$, i.e., $\lfloor -a \rfloor = -\lceil a \rceil$.

Int.ceil_neg theorem

: ⌈-a⌉ = -⌊a⌋

Full source

theorem ceil_neg : ⌈-a⌉ = -⌊a⌋ :=
  eq_of_forall_ge_iff fun z => by rw [neg_le, ceil_le, le_floor, Int.cast_neg, neg_le]

Ceiling of Negative Equals Negative Floor: $\lceil -a \rceil = -\lfloor a \rfloor$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the ceiling of $-a$ equals the negation of the floor of $a$, i.e., $\lceil -a \rceil = -\lfloor a \rfloor$.

Int.ceil_intCast theorem

(z : ℤ) : ⌈(z : R)⌉ = z

Full source

@[simp]
theorem ceil_intCast (z : ℤ) : ⌈(z : R)⌉ = z :=
  eq_of_forall_ge_iff fun a => by rw [ceil_le, Int.cast_le]

Ceiling of Integer Cast: $\lceil z \rceil = z$

Informal description

For any integer $z$, the ceiling function evaluated at $z$ (viewed as an element of a linearly ordered ring $R$) returns $z$ itself, i.e., $\lceil z \rceil = z$.

Int.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_natCast, cast_le]

Ceiling of Natural Number Cast: $\lceil n \rceil = n$

Informal description

For any natural number $n$ and any linearly ordered ring $R$, the ceiling of the canonical embedding of $n$ into $R$ equals $n$ itself, i.e., $\lceil n \rceil = n$.

Int.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 Numeric Literal ≥ 2: $\lceil n \rceil = n$

Informal description

For any natural number $n \geq 2$ and any linearly ordered ring $R$, the ceiling of the canonical embedding of $n$ into $R$ equals $n$ itself, i.e., $\lceil n \rceil = n$.

Int.ceil_add_intCast theorem

(a : R) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z

Full source

@[simp]
theorem ceil_add_intCast (a : R) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z := by
  rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]

Ceiling Function Additivity with Integer Addition: $\lceil a + z \rceil = \lceil a \rceil + z$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $z$, the ceiling of $a + z$ equals the ceiling of $a$ plus $z$, i.e., $\lceil a + z \rceil = \lceil a \rceil + z$.

Int.ceil_add_natCast theorem

(a : R) (n : ℕ) : ⌈a + n⌉ = ⌈a⌉ + n

Full source

@[simp]
theorem ceil_add_natCast (a : R) (n : ℕ) : ⌈a + n⌉ = ⌈a⌉ + n := by
  rw [← Int.cast_natCast, ceil_add_intCast]

Ceiling Function Additivity with Natural Number Addition: $\lceil a + n \rceil = \lceil a \rceil + n$

Informal description

For any element $a$ in a linearly ordered ring $R$ 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$.

Int.ceil_add_one theorem

(a : R) : ⌈a + 1⌉ = ⌈a⌉ + 1

Full source

@[simp]
theorem ceil_add_one (a : R) : ⌈a + 1⌉ = ⌈a⌉ + 1 := by
  rw [← ceil_add_intCast a (1 : ℤ), cast_one]

Ceiling Function Additivity with One: $\lceil a + 1 \rceil = \lceil a \rceil + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling of $a + 1$ equals the ceiling of $a$ plus $1$, i.e., $\lceil a + 1 \rceil = \lceil a \rceil + 1$.

Int.ceil_add_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : ⌈a + ofNat(n)⌉ = ⌈a⌉ + ofNat(n)

Full source

@[simp]
theorem ceil_add_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌈a + ofNat(n)⌉ = ⌈a⌉ + ofNat(n) :=
  ceil_add_natCast a n

Ceiling Function Additivity with Numerals ≥ 2: $\lceil a + n \rceil = \lceil a \rceil + n$

Informal description

For any element $a$ in a linearly ordered ring $R$ 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$.

Int.ceil_sub_intCast theorem

(a : R) (z : ℤ) : ⌈a - z⌉ = ⌈a⌉ - z

Full source

@[simp]
theorem ceil_sub_intCast (a : R) (z : ℤ) : ⌈a - z⌉ = ⌈a⌉ - z :=
  Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (ceil_add_intCast _ _)

Ceiling Function Additivity with Integer Subtraction: $\lceil a - z \rceil = \lceil a \rceil - z$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any integer $z$, the ceiling of $a - z$ equals the ceiling of $a$ minus $z$, i.e., $\lceil a - z \rceil = \lceil a \rceil - z$.

Int.ceil_sub_natCast theorem

(a : R) (n : ℕ) : ⌈a - n⌉ = ⌈a⌉ - n

Full source

@[simp]
theorem ceil_sub_natCast (a : R) (n : ℕ) : ⌈a - n⌉ = ⌈a⌉ - n := by
  convert ceil_sub_intCast a n using 1
  simp

Ceiling Function Additivity with Natural Number Subtraction: $\lceil a - n \rceil = \lceil a \rceil - n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n$, the ceiling of $a - n$ equals the ceiling of $a$ minus $n$, i.e., $\lceil a - n \rceil = \lceil a \rceil - n$.

Int.ceil_sub_one theorem

(a : R) : ⌈a - 1⌉ = ⌈a⌉ - 1

Full source

@[simp]
theorem ceil_sub_one (a : R) : ⌈a - 1⌉ = ⌈a⌉ - 1 := by
  rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]

Ceiling Function Additivity with Subtraction of One: $\lceil a - 1 \rceil = \lceil a \rceil - 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling of $a - 1$ equals the ceiling of $a$ minus $1$, i.e., $\lceil a - 1 \rceil = \lceil a \rceil - 1$.

Int.ceil_sub_ofNat theorem

(a : R) (n : ℕ) [n.AtLeastTwo] : ⌈a - ofNat(n)⌉ = ⌈a⌉ - ofNat(n)

Full source

@[simp]
theorem ceil_sub_ofNat (a : R) (n : ℕ) [n.AtLeastTwo] :
    ⌈a - ofNat(n)⌉ = ⌈a⌉ - ofNat(n) :=
  ceil_sub_natCast a n

Ceiling Function Additivity with Subtraction of $n \geq 2$: $\lceil a - n \rceil = \lceil a \rceil - n$

Informal description

For any element $a$ in a linearly ordered ring $R$ and any natural number $n \geq 2$, the ceiling of $a - n$ equals the ceiling of $a$ minus $n$, i.e., $\lceil a - n \rceil = \lceil a \rceil - n$.

Int.ceil_lt_add_one theorem

(a : R) : (⌈a⌉ : R) < a + 1

Full source

@[bound]
theorem ceil_lt_add_one (a : R) : (⌈a⌉ : R) < a + 1 := by
  rw [← lt_ceil, ← Int.cast_one, ceil_add_intCast]
  apply lt_add_one

Ceiling Bound: $\lceil a \rceil < a + 1$

Informal description

For any element $a$ in a linearly ordered ring $R$, the canonical embedding of the ceiling of $a$ into $R$ is strictly less than $a + 1$, i.e., $\lceil a \rceil < a + 1$.

Int.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, Int.cast_add]
  gcongr <;> apply le_ceil

Subadditivity of the Ceiling Function: $\lceil a + b \rceil \leq \lceil a \rceil + \lceil b \rceil$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the ceiling of their sum satisfies $\lceil a + b \rceil \leq \lceil a \rceil + \lceil b \rceil$.

Int.ceil_add_ceil_le theorem

(a b : R) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Full source

@[bound]
theorem ceil_add_ceil_le (a b : R) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1 := by
  rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
  refine (ceil_lt_add_one _).le.trans ?_
  rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
  exact le_ceil _

Ceiling Sum Inequality: $\lceil a \rceil + \lceil b \rceil \leq \lceil a + b \rceil + 1$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the sum of their ceilings is less than or equal to the ceiling of their sum plus one, i.e., $\lceil a \rceil + \lceil b \rceil \leq \lceil a + b \rceil + 1$.

Int.ceil_zero theorem

: ⌈(0 : R)⌉ = 0

Full source

@[simp]
theorem ceil_zero : ⌈(0 : R)⌉ = 0 := by rw [← cast_zero, ceil_intCast]

Ceiling of Zero: $\lceil 0 \rceil = 0$

Informal description

For any linearly ordered ring $R$, the ceiling function evaluated at $0$ returns $0$, i.e., $\lceil 0 \rceil = 0$.

Int.ceil_one theorem

: ⌈(1 : R)⌉ = 1

Full source

@[simp]
theorem ceil_one : ⌈(1 : R)⌉ = 1 := by rw [← cast_one, ceil_intCast]

Ceiling of One: $\lceil 1 \rceil = 1$

Informal description

For any linearly ordered ring $R$ with a ceiling function, the ceiling of the multiplicative identity element $1$ is equal to $1$, i.e., $\lceil 1 \rceil = 1$.

Int.ceil_eq_on_Ioc' theorem

(z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z

Full source

theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z := fun a ha =>
  mod_cast ceil_eq_on_Ioc z a ha

Ceiling Function Identity on $(z-1, z]$

Informal description

For any integer $z$ and any element $a$ in the interval $(z-1, z]$ of a linearly ordered ring $R$, the ceiling function satisfies $\lceil a \rceil = z$ (where $\lceil a \rceil$ is viewed as an element of $R$ via the canonical embedding of integers into $R$).

Int.ceil_eq_self_iff_mem theorem

(a : R) : ⌈a⌉ = a ↔ a ∈ Set.range Int.cast

Full source

lemma ceil_eq_self_iff_mem (a : R) : ⌈a⌉⌈a⌉ = a ↔ a ∈ Set.range Int.cast := by
  aesop

Ceiling Equals Self iff Integer: $\lceil a \rceil = a \leftrightarrow a \in \mathbb{Z}$

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling of $a$ equals $a$ if and only if $a$ is an integer (i.e., $a$ is in the range of the integer casting function). In other words, $\lceil a \rceil = a \leftrightarrow a \in \mathbb{Z}$.

Int.floor_le_ceil theorem

(a : R) : ⌊a⌋ ≤ ⌈a⌉

Full source

@[bound]
theorem floor_le_ceil (a : R) : ⌊a⌋ ≤ ⌈a⌉ :=
  cast_le.1 <| (floor_le _).trans <| le_ceil _

Floor-Ceiling Inequality: $\lfloor a \rfloor \leq \lceil a \rceil$

Informal description

For any element $a$ in a linearly ordered ring $R$, the floor of $a$ is less than or equal to its ceiling, i.e., $\lfloor a \rfloor \leq \lceil a \rceil$.

Int.floor_lt_ceil_of_lt theorem

{a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉

Full source

@[bound]
theorem floor_lt_ceil_of_lt {a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=
  cast_lt.1 <| (floor_le a).trans_lt <| h.trans_le <| le_ceil b

Floor-Ceiling Inequality for Strictly Ordered Elements: $\lfloor a \rfloor < \lceil b \rceil$ when $a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$ with $a < b$, the floor of $a$ is strictly less than the ceiling of $b$, i.e., $\lfloor a \rfloor < \lceil b \rceil$.

Int.ceil_eq_floor_add_one_iff_not_mem theorem

(a : R) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast

Full source

lemma ceil_eq_floor_add_one_iff_not_mem (a : R) : ⌈a⌉⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast := by
  refine ⟨fun h ht => ?_, fun h => ?_⟩
  · have := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
    linarith [Int.cast_inj.mp this]
  · apply le_antisymm (Int.ceil_le_floor_add_one _)
    rw [Int.add_one_le_ceil_iff]
    exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

Ceiling-Floor Gap Characterization for Non-Integers

Informal description

For any element $a$ in a linearly ordered ring $R$, the ceiling of $a$ equals the floor of $a$ plus one if and only if $a$ is not an integer (i.e., $a$ is not in the range of the canonical embedding $\mathbb{Z} \to R$). In other words: $$\lceil a \rceil = \lfloor a \rfloor + 1 \leftrightarrow a \notin \mathbb{Z}$$

Int.fract_eq_zero_or_add_one_sub_ceil theorem

(a : R) : fract a = 0 ∨ fract a = a + 1 - (⌈a⌉ : R)

Full source

theorem fract_eq_zero_or_add_one_sub_ceil (a : R) : fractfract a = 0 ∨ fract a = a + 1 - (⌈a⌉ : R) := by
  rcases eq_or_ne (fract a) 0 with ha | ha
  · exact Or.inl ha
  right
  suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
    rw [this, ← self_sub_fract]
    abel
  norm_cast
  rw [ceil_eq_iff]
  refine ⟨?_, _root_.le_of_lt <| by simp⟩
  rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
  exact ha.symm.lt_of_le (fract_nonneg a)

Characterization of Fractional Part: $\operatorname{fract}(a) = 0$ or $a + 1 - \lceil a \rceil$

Informal description

For any element $a$ in a linearly ordered ring $R$, the fractional part $\operatorname{fract}(a)$ satisfies either $\operatorname{fract}(a) = 0$ or $\operatorname{fract}(a) = a + 1 - \lceil a \rceil$, where $\lceil a \rceil$ is the ceiling of $a$ (viewed as an element of $R$ via the canonical embedding).

Int.ceil_eq_add_one_sub_fract theorem

(ha : fract a ≠ 0) : (⌈a⌉ : R) = a + 1 - fract a

Full source

theorem ceil_eq_add_one_sub_fract (ha : fractfract a ≠ 0) : (⌈a⌉ : R) = a + 1 - fract a := by
  rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
  abel

Ceiling as $a + 1 - \operatorname{fract}(a)$ for Non-Integer Values

Informal description

For any element $a$ in a linearly ordered ring $R$ with $\operatorname{fract}(a) \neq 0$, the ceiling of $a$ (viewed as an element of $R$) satisfies $\lceil a \rceil = a + 1 - \operatorname{fract}(a)$, where $\operatorname{fract}(a) = a - \lfloor a \rfloor$ is the fractional part of $a$.

Int.ceil_sub_self_eq theorem

(ha : fract a ≠ 0) : (⌈a⌉ : R) - a = 1 - fract a

Full source

theorem ceil_sub_self_eq (ha : fractfract a ≠ 0) : (⌈a⌉ : R) - a = 1 - fract a := by
  rw [(or_iff_right ha).mp (fract_eq_zero_or_add_one_sub_ceil a)]
  abel

Ceiling Difference Formula: $\lceil a \rceil - a = 1 - \operatorname{fract}(a)$ when $\operatorname{fract}(a) \neq 0$

Informal description

For any element $a$ in a linearly ordered ring $R$ with fractional part $\operatorname{fract}(a) \neq 0$, the difference between the ceiling of $a$ (viewed as an element of $R$) and $a$ itself equals $1 - \operatorname{fract}(a)$. That is: $$ \lceil a \rceil - a = 1 - \operatorname{fract}(a) $$

Int.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
      rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
        ← ceil_le, le_floor]

Inequality for Product with Floor: $b \cdot a < \lfloor a \rfloor$ under $0 < b < 1$ and $\lceil \frac{b}{1 - b} \rceil \leq a$

Informal description

Let $R$ be a linearly ordered ring, and let $a, b \in R$ such that $0 < b < 1$ and $\lceil \frac{b}{1 - b} \rceil \leq a$. Then $b \cdot a < \lfloor a \rfloor$.

Int.ceil_div_ceil_inv_sub_one theorem

(ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Full source

lemma ceil_div_ceil_inv_sub_one (ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉ := by
  obtain rfl | ha := ha.eq_or_lt
  · simp
  have : 0 < a - 1 := by linarith
  refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
  rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
    ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]
  convert ceil_lt_add_one (R := k) _ using 1
  field_simp

Ceiling Identity for $\lceil (a - 1)^{-1} \rceil / a$ when $a \geq 1$

Informal description

For any element $a$ in a linearly ordered ring with $1 \leq a$, the ceiling of the quotient of $\lceil (a - 1)^{-1} \rceil$ divided by $a$ equals $\lceil (a - 1)^{-1} \rceil$, i.e., $$ \left\lceil \frac{\lceil (a - 1)^{-1} \rceil}{a} \right\rceil = \lceil (a - 1)^{-1} \rceil. $$

Int.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 _
      _ = 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 Bound under Multiplication: $\lceil a \rceil < b \cdot a$ for $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} < a$

Informal description

Let $R$ be a linearly ordered ring, and let $a, b \in R$ such that $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} < a$. Then the ceiling of $a$ satisfies $\lceil a \rceil < b \cdot a$.

Int.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 [ceil_div_ceil_inv_sub_one hb.le, mul_div_cancel₀]
    positivity
  · exact (ceil_lt_mul hb hba).le

Ceiling Bound under Multiplication: $\lceil a \rceil \leq b \cdot a$ for $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} \leq a$

Informal description

Let $R$ be a linearly ordered ring, and let $a, b \in R$ such that $b > 1$ and $\frac{\lceil (b - 1)^{-1} \rceil}{b} \leq a$. Then the ceiling of $a$ satisfies $\lceil a \rceil \leq b \cdot a$.

Int.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

Half of an Element is Less Than Its Floor When $1 \leq a$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ such that $1 \leq a$, the half of $a$ is strictly less than the floor of $a$, i.e., $a / 2 < \lfloor a \rfloor$.

Int.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 under doubling: $\lceil a \rceil < 2a$ for $a > \frac{1}{2}$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ such that $2^{-1} < a$, the ceiling of $a$ satisfies $\lceil a \rceil < 2a$.

Int.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 bound under doubling: $\lceil a \rceil \leq 2a$ for $a \geq \frac{1}{2}$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ such that $2^{-1} \leq a$, the ceiling of $a$ satisfies $\lceil a \rceil \leq 2a$.

Int.preimage_Ioo theorem

{a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉

Full source

@[simp]
theorem preimage_Ioo {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉ := by
  ext
  simp [floor_lt, lt_ceil]

Preimage of Open Interval under Integer Embedding Equals Floor-Ceiling Interval

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the preimage of the open interval $(a, b)$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the open interval $(\lfloor a \rfloor, \lceil b \rceil)$ in $\mathbb{Z}$.

Int.preimage_Ico theorem

{a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉

Full source

@[simp]
theorem preimage_Ico {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉ := by
  ext
  simp [ceil_le, lt_ceil]

Preimage of $[a, b)$ under Integer Embedding Equals $[\lceil a \rceil, \lceil b \rceil)$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the preimage of the left-closed right-open interval $[a, b)$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the left-closed right-open interval $[\lceil a \rceil, \lceil b \rceil)$ in $\mathbb{Z}$.

Int.preimage_Ioc theorem

{a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋

Full source

@[simp]
theorem preimage_Ioc {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋ := by
  ext
  simp [floor_lt, le_floor]

Preimage of $(a, b]$ under Integer Embedding Equals $(\lfloor a \rfloor, \lfloor b \rfloor]$

Informal description

For any elements $a$ and $b$ in a linearly ordered ring $R$, the preimage of the left-open right-closed interval $(a, b]$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the left-open right-closed interval $(\lfloor a \rfloor, \lfloor b \rfloor]$ in $\mathbb{Z}$.

Int.preimage_Icc theorem

{a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋

Full source

@[simp]
theorem preimage_Icc {a b : R} : ((↑) : ℤ → R) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋ := by
  ext
  simp [ceil_le, le_floor]

Preimage of Closed Interval under Integer Embedding Equals Integer Interval Between Ceiling and Floor

Informal description

For any real numbers $a$ and $b$, the preimage of the closed interval $[a, b]$ under the canonical embedding of integers into reals is equal to the closed interval of integers $[\lceil a \rceil, \lfloor b \rfloor]$. That is, $$ \{ z \in \mathbb{Z} \mid a \leq z \leq b \} = [\lceil a \rceil, \lfloor b \rfloor] \cap \mathbb{Z}. $$

Int.preimage_Ioi theorem

: ((↑) : ℤ → R) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋

Full source

@[simp]
theorem preimage_Ioi : ((↑) : ℤ → R) ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋ := by
  ext
  simp [floor_lt]

Preimage of $(a, \infty)$ under Integer Embedding Equals $(\lfloor a \rfloor, \infty)$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the preimage of the right-infinite open interval $(a, \infty)$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the right-infinite open interval $(\lfloor a \rfloor, \infty)$ in $\mathbb{Z}$. In other words, for any integer $z$, $z > a$ if and only if $z > \lfloor a \rfloor$.

Int.preimage_Ici theorem

: ((↑) : ℤ → R) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉

Full source

@[simp]
theorem preimage_Ici : ((↑) : ℤ → R) ⁻¹' Set.Ici a = Set.Ici ⌈a⌉ := by
  ext
  simp [ceil_le]

Preimage of $[a, \infty)$ under Integer Embedding Equals $[\lceil a \rceil, \infty)$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the preimage of the left-closed right-infinite interval $[a, \infty)$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the left-closed right-infinite interval $[\lceil a \rceil, \infty)$ in $\mathbb{Z}$. In other words, for any integer $z$, $z \geq a$ if and only if $z \geq \lceil a \rceil$.

Int.preimage_Iio theorem

: ((↑) : ℤ → R) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉

Full source

@[simp]
theorem preimage_Iio : ((↑) : ℤ → R) ⁻¹' Set.Iio a = Set.Iio ⌈a⌉ := by
  ext
  simp [lt_ceil]

Preimage of $(a, \infty)$ under Integer Embedding Equals $(\lceil a \rceil, \infty)$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the preimage of the open interval $(a, \infty)$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the open interval $(\lceil a \rceil, \infty)$ in $\mathbb{Z}$. In other words, for any integer $z$, $z > a$ if and only if $z > \lceil a \rceil$.

Int.preimage_Iic theorem

: ((↑) : ℤ → R) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋

Full source

@[simp]
theorem preimage_Iic : ((↑) : ℤ → R) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋ := by
  ext
  simp [le_floor]

Preimage of $(-\infty, a]$ under Integer Embedding Equals $(-\infty, \lfloor a \rfloor]$

Informal description

For any element $a$ in a linearly ordered ring $R$ with a floor function, the preimage of the closed interval $(-\infty, a]$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the closed interval $(-\infty, \lfloor a \rfloor]$ in $\mathbb{Z}$. In other words, for any integer $z$, $z \leq a$ if and only if $z \leq \lfloor a \rfloor$.

Int.floor_congr theorem

(h : ∀ n : ℤ, (n : R) ≤ a ↔ (n : S) ≤ b) : ⌊a⌋ = ⌊b⌋

Full source

theorem floor_congr (h : ∀ n : ℤ, (n : R) ≤ a ↔ (n : S) ≤ b) : ⌊a⌋ = ⌊b⌋ :=
  (le_floor.2 <| (h _).1 <| floor_le _).antisymm <| le_floor.2 <| (h _).2 <| floor_le _

Floor Function Equality under Equivalent Integer Bounds

Informal description

Let $R$ and $S$ be linearly ordered rings with floor functions. Given elements $a \in R$ and $b \in S$, if for every integer $n$ the inequality $(n : R) \leq a$ holds if and only if $(n : S) \leq b$ holds, then the floor functions of $a$ and $b$ are equal, i.e., $\lfloor a \rfloor = \lfloor b \rfloor$.

Int.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 Integer Bounds

Informal description

For any two elements $a$ and $b$ in a linearly ordered ring $\alpha$, if for every integer $n$ the inequalities $a \leq n$ and $b \leq n$ are equivalent, then their ceiling values are equal, i.e., $\lceil a \rceil = \lceil b \rceil$.

Int.map_floor theorem

(f : F) (hf : StrictMono f) (a : R) : ⌊f a⌋ = ⌊a⌋

Full source

theorem map_floor (f : F) (hf : StrictMono f) (a : R) : ⌊f a⌋ = ⌊a⌋ :=
  floor_congr fun n => by rw [← map_intCast f, hf.le_iff_le]

Floor Preservation under Strictly Monotone Functions

Informal description

Let $R$ be a linearly ordered ring with a floor function, and let $F$ be a function-like type. Given a strictly monotone function $f : F$ and an element $a \in R$, the floor of $f(a)$ is equal to the floor of $a$, i.e., $\lfloor f(a) \rfloor = \lfloor a \rfloor$.

Int.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_intCast f, hf.le_iff_le]

Ceiling Preservation under Strictly Increasing Functions

Informal description

Let $R$ be a linearly ordered ring and $F$ a type with a function-like structure mapping $R$ to itself. Given a strictly increasing function $f : F$ and an element $a \in R$, the ceiling of $f(a)$ equals the ceiling of $a$, i.e., $\lceil f(a) \rceil = \lceil a \rceil$.

Int.map_fract theorem

(f : F) (hf : StrictMono f) (a : R) : fract (f a) = f (fract a)

Full source

theorem map_fract (f : F) (hf : StrictMono f) (a : R) : fract (f a) = f (fract a) := by
  simp_rw [fract, map_sub, map_intCast, map_floor _ hf]

Fractional Part Preservation under Strictly Increasing Functions: $\text{fract}(f(a)) = f(\text{fract}(a))$

Informal description

Let $R$ be a linearly ordered ring with a floor function, and let $F$ be a function-like type. Given a strictly increasing function $f : F$ and an element $a \in R$, the fractional part of $f(a)$ is equal to $f$ applied to the fractional part of $a$, i.e., $\text{fract}(f(a)) = f(\text{fract}(a))$.

Int.natCast_floor_eq_floor theorem

(ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋

Full source

theorem Int.natCast_floor_eq_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋ := by
  rw [← Int.floor_toNat, Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)]

Equality of Natural and Integer Floor for Non-Negative Elements

Informal description

For any non-negative element $a$ in a linearly ordered ring $\alpha$, the integer obtained by casting the natural floor $\lfloor a \rfloor_\mathbb{N}$ to $\mathbb{Z}$ is equal to the integer floor $\lfloor a \rfloor$, i.e., $(\lfloor a \rfloor_\mathbb{N} : \mathbb{Z}) = \lfloor a \rfloor$.

Int.natCast_ceil_eq_ceil theorem

(ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉

Full source

theorem Int.natCast_ceil_eq_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
  rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]

Equality of Natural and Integer Ceiling for Non-Negative Elements

Informal description

For any non-negative element $a$ in a linearly ordered ring $\alpha$, the integer obtained by casting the natural ceiling $\lceil a \rceil_\mathbb{N}$ to $\mathbb{Z}$ is equal to the integer ceiling $\lceil a \rceil$, i.e., $(\lceil a \rceil_\mathbb{N} : \mathbb{Z}) = \lceil a \rceil$.

Int.natCast_ceil_eq_ceil_of_neg_one_lt theorem

(ha : -1 < a) : (⌈a⌉₊ : ℤ) = ⌈a⌉

Full source

theorem Int.natCast_ceil_eq_ceil_of_neg_one_lt (ha : -1 < a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ := by
  rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt ha)]

Equality of Natural and Integer Ceilings for Elements Greater Than Negative One

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ with $-1 < a$, the natural ceiling $\lceil a \rceil_\mathbb{N}$ cast to the integers equals the integer ceiling $\lceil a \rceil$, i.e., $(\lceil a \rceil_\mathbb{N} : \mathbb{Z}) = \lceil a \rceil$.

natCast_floor_eq_intCast_floor theorem

(ha : 0 ≤ a) : (⌊a⌋₊ : R) = ⌊a⌋

Full source

theorem natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : R) = ⌊a⌋ := by
  rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

Equality of Natural and Integer Floor Casts for Non-Negative Elements

Informal description

For any non-negative element $a$ in a linearly ordered ring $R$, the natural floor $\lfloor a \rfloor_\mathbb{N}$ cast to $R$ equals the integer floor $\lfloor a \rfloor$ in $R$, i.e., $(\lfloor a \rfloor_\mathbb{N} : R) = \lfloor a \rfloor$.

natCast_ceil_eq_intCast_ceil theorem

(ha : 0 ≤ a) : (⌈a⌉₊ : R) = ⌈a⌉

Full source

theorem natCast_ceil_eq_intCast_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : R) = ⌈a⌉ := by
  rw [← Int.natCast_ceil_eq_ceil ha, Int.cast_natCast]

Equality of Natural and Integer Ceiling Casts for Non-Negative Elements

Informal description

For any non-negative element $a$ in a linearly ordered ring $R$, the natural ceiling $\lceil a \rceil_\mathbb{N}$ cast to $R$ equals the integer ceiling $\lceil a \rceil$ in $R$, i.e., $(\lceil a \rceil_\mathbb{N} : R) = \lceil a \rceil$.

natCast_ceil_eq_intCast_ceil_of_neg_one_lt theorem

(ha : -1 < a) : (⌈a⌉₊ : R) = ⌈a⌉

Full source

theorem natCast_ceil_eq_intCast_ceil_of_neg_one_lt (ha : -1 < a) : (⌈a⌉₊ : R) = ⌈a⌉ := by
  rw [← Int.natCast_ceil_eq_ceil_of_neg_one_lt ha, Int.cast_natCast]

Natural and Integer Ceilings Coincide for $a > -1$ in Linearly Ordered Rings

Informal description

For any element $a$ in a linearly ordered ring $R$ with $-1 < a$, the natural ceiling $\lceil a \rceil_\mathbb{N}$ cast to $R$ equals the integer ceiling $\lceil a \rceil$ in $R$, i.e., $(\lceil a \rceil_\mathbb{N} : R) = \lceil a \rceil$.

subsingleton_floorRing theorem

{R} [Ring R] [LinearOrder R] : Subsingleton (FloorRing R)

Full source

/-- There exists at most one `FloorRing` structure on a given linear ordered ring. -/
theorem subsingleton_floorRing {R} [Ring R] [LinearOrder R] : Subsingleton (FloorRing R) := by
  refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.floor = H₂.floor :=
    funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
  cases H₁; cases H₂; congr

Uniqueness of FloorRing Structure on a Linearly Ordered Ring

Informal description

For any linearly ordered ring $R$, there exists at most one `FloorRing` structure on $R$.

Mathlib.Algebra.Order.Floor.Ring

TODO

Tags