Int.sub_one_lt_floor
theorem Int.sub_one_lt_floor :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), a - 1 < ↑⌊a⌋
This theorem states that for any type `α` which is a linearly ordered ring and has the structure of a floor ring, the result of subtracting 1 from any element `a` of type `α` is strictly less than the floor of `a`. In mathematical terms, for any real number `a`, we have `a - 1 < ⌊a⌋`, where `⌊a⌋` denotes the greatest integer less than or equal to `a` (the floor function).
More concisely: For any linearly ordered ring `α` with a floor structure, the floor function applied to an element `a` is strictly less than `a - 1`. (In symbols: `⌊a⌋ < a - 1`).
|
Int.floor_le
theorem Int.floor_le : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), ↑⌊a⌋ ≤ a := by
sorry
This theorem, `Int.floor_le`, asserts that for any type `α` that is a linearly ordered ring and also a floor ring, the floor of any element `a` of type `α` is less than or equal to `a`. In mathematical terms, for every `a` in `α`, `⌊a⌋ ≤ a`. Here, `⌊a⌋` represents the greatest integer less than or equal to `a`, known as the floor of `a`.
More concisely: For any element `a` in a linearly ordered ring and floor ring `α`, the floor of `a`, `⌊a⌋`, is less than or equal to `a`.
|
FloorSemiring.floor_of_neg
theorem FloorSemiring.floor_of_neg :
∀ {α : Type u_4} [inst : OrderedSemiring α] [self : FloorSemiring α] {a : α}, a < 0 → FloorSemiring.floor a = 0
The theorem `FloorSemiring.floor_of_neg` states that for any ordered semiring `α` and any element `a` of `α`, if `a` is less than zero, then the floor of `a` is zero. Here, the floor of `a` is defined as the greatest natural number `n` such that `n` is less than or equal to `a`. In other words, for any negative element in an ordered semiring, its floor is zero.
More concisely: For any ordered semiring `α` and element `a` in `α`, if `a` is negative then the floor of `a` equals `0`.
|
round_add_int
theorem round_add_int :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (x : α) (y : ℤ),
round (x + ↑y) = round x + y
The theorem `round_add_int` states that for all types `α` that form a linear ordered ring with a floor function, for any real number `x` and integer `y`, rounding the sum of `x` and `y` is the same as rounding `x` and then adding `y`. In other words, the `round` function distributes over integer addition.
More concisely: For all types `α` that form a linear ordered ring with a floor function, the rounding of `(x : α) + y` equals `round x + y` for all real numbers `x` and integers `y`.
|
Int.lt_ceil
theorem Int.lt_ceil :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, z < ⌈a⌉ ↔ ↑z < a
This theorem, `Int.lt_ceil`, states that for any integer `z` and any number `a` of a certain type `α` (where `α` is a type that forms a linear ordered ring and also has a floor ring structure), `z` is less than the ceiling of `a` if and only if the real number equivalent of `z` is less than `a`. In other words, it establishes a relationship between the integer less-than operation and the real number less-than operation when dealing with the ceiling function.
More concisely: For any integer `z` and real number `a` from a type `α` that is a linear ordered ring with a floor ring structure, `z < ceil a` if and only if `to_real z < a`.
|
round_eq
theorem round_eq :
∀ {α : Type u_2} [inst : LinearOrderedField α] [inst_1 : FloorRing α] (x : α), round x = ⌊x + 1 / 2⌋
This theorem states that for any type `α` that is a linear ordered field and has a floor ring structure (which basically means that we can talk about the "floor" or "greatest integer less than or equal to" operation for elements of type `α`), the rounding operation for any element `x` of type `α` can be expressed as the floor of `x` plus 1/2. In other words, to round a number `x` to the nearest integer, you can instead add 1/2 to `x` and then take the floor of the result.
More concisely: For any linear ordered field `α` with a floor ring structure, the rounding operation on `α` equals the floor function followed by adding one-half.
|
Int.floor_mono
theorem Int.floor_mono : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], Monotone Int.floor := by
sorry
The theorem `Int.floor_mono` states that for any type `α` that is equipped with a linear ordered ring structure and a floor ring structure, the `Int.floor` function is monotone. This means that if `a` and `b` are two elements of `α` such that `a ≤ b`, then the greatest integer less than or equal to `a` is also less than or equal to the greatest integer less than or equal to `b`. In mathematical notation, this is equivalent to saying that if `a ≤ b`, then `⌊a⌋ ≤ ⌊b⌋`, where `⌊x⌋` denotes the floor of `x`.
More concisely: If `α` is a type equipped with a linear ordered ring structure and a floor ring structure, then the floor function `Int.floor` is monotone, that is, `⌊a⌋ ≤ ⌊b⌋` for all `a ≤ b` in `α`.
|
Int.ceil_le
theorem Int.ceil_le :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, ⌈a⌉ ≤ z ↔ a ≤ ↑z
This theorem, `Int.ceil_le`, states that for any type `α` which is a linearly ordered ring and also a floor ring, and any integer `z` and element `a` of type `α`, the ceiling (the smallest integer greater than or equal to `a`) of `a` is less than or equal to `z` if and only if `a` is less than or equal to the integer version of `z`. Essentially, it describes the relationship between the ceiling function and inequality in the context of ordered rings.
More concisely: For any linearly ordered ring and floor ring type `α`, and integers `z` and `a` of type `α`, `ceil a <= z` if and only if `a <= to_int z`.
|
Nat.ceil_lt_add_one
theorem Nat.ceil_lt_add_one :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α}, 0 ≤ a → ↑⌈a⌉₊ < a + 1 := by
sorry
This theorem, `Nat.ceil_lt_add_one`, states that for any non-negative real number `a` (denoted as `α`), the ceiling function of `a` (denoted as `⌈a⌉₊`) when converted back to real number, is strictly less than `a` plus one. In other words, the ceiling of any non-negative real number is always less than the next integer in the number line. This is applicable in the context of a linearly ordered semiring and a floor semiring.
More concisely: For any non-negative real number `α`, the ceiling function `⌈α⌉₊` satisfies `⌈α⌉₊ < α + 1`.
|
Nat.lt_of_floor_lt
theorem Nat.lt_of_floor_lt :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ}, ⌊a⌋₊ < n → a < ↑n
This theorem asserts that for any type `α` which is a linearly ordered semiring and has a floor function, and for any value `a` of type `α` and natural number `n`, if the floor of `a` is less than `n`, then `a` itself is also less than `n`. In mathematical terms, if $⌊a⌋₊ < n$ then $a < n$.
More concisely: If `α` is a linearly ordered semiring with a floor function, then for all `a : α` and `n : ℕ`, if `⌊a⌋ < n`, then `a < n`.
|
Int.floor_sub_int
theorem Int.floor_sub_int :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (z : ℤ), ⌊a - ↑z⌋ = ⌊a⌋ - z
This theorem states that for any type `α` which is a linear ordered ring and has a floor function (i.e., the largest integer less than or equal to a real number), and for any element `a` of this type and any integer `z`, the floor of the difference between `a` and `z` (when `z` is considered as an element of the type `α` using the coercion function) is equal to the difference between the floor of `a` and `z`. In LaTeX terms, this reads: For all $a$ in $α$ and $z$ in $\mathbb{Z}$, $⌊a - z⌋ = ⌊a⌋ - z$.
More concisely: For any linear ordered ring `α` with a floor function and for all `a` in `α` and `z` in `ℤ`, `⌊a - z⌋ = ⌊a⌋ - z`.
|
Nat.ceil_mono
theorem Nat.ceil_mono :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α], Monotone Nat.ceil
This theorem states that for any type `α` that is a linear ordered semiring (a structure with two operations satisfying certain properties, such as the distributivity of one operation over the other, and the existence of a total ordering compatible with the operations) and a floor semiring (a structure that allows us to round elements down to the nearest integer), the function `Nat.ceil` is monotone. In other words, if `a ≤ b` for any `a` and `b` of type `α`, then `⌈a⌉₊ ≤ ⌈b⌉₊`, where `⌈x⌉₊` denotes the least natural number `n` such that `x ≤ n`.
More concisely: For any linear ordered semiring `α` and floor semiring `α`, the monotonicity function `x ↦ ⌈x⌉₊` is increasing on `α`.
|
Int.floor_add_int
theorem Int.floor_add_int :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (z : ℤ), ⌊a + ↑z⌋ = ⌊a⌋ + z
This theorem states that for any type `α` that is a linear ordered ring and also a floor ring, and for any element `a` of type `α` and integer `z`, the floor of the sum of `a` and `z` (where `z` is coerced to type `α`) is equal to the sum of the floor of `a` and `z`. In mathematical terms, it means that for any real number `a` and any integer `z`, ⌊a + z⌋ = ⌊a⌋ + z.
More concisely: For any linear ordered ring and floor ring type `α` and its element `a` of type `α` and integer `z`, the floor of their sum is equal to the sum of their floors: `⌊a + z⌋ = ⌊a⌋ + z`.
|
Mathlib.Algebra.Order.Floor._auxLemma.36
theorem Mathlib.Algebra.Order.Floor._auxLemma.36 :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, (z < ⌈a⌉) = (↑z < a) := by
sorry
This theorem, under the Mathlib algebra order floor module, states that for any type `α` that forms a linearly ordered ring and a floor ring, and for any integer `z` and element `a` of type `α`, `z` is less than the ceiling of `a` if and only if the real number equivalent of `z` is less than `a`. In essence, it establishes a relationship between the inequality of an integer and a real number with the inequality of that integer and the ceiling of the real number.
More concisely: For any linearly ordered ring and floor ring type `α`, and for any integer `z` and element `a` of `α`, `z < ceiling a` if and only if `toReal z < a`.
|
Nat.floor_mono
theorem Nat.floor_mono :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α], Monotone Nat.floor
The theorem `Nat.floor_mono` states that for any type `α` with a linear ordering and a floor structure (i.e., we can "round down" elements of `α` to the nearest whole number), the function `Nat.floor`, which takes an element of `α` and returns the greatest natural number less than or equal to it, is monotone. This means that if `a` and `b` are elements of `α` and `a` is less than or equal to `b`, then the floor of `a` is less than or equal to the floor of `b`.
More concisely: For any type `α` with a linear ordering and a floor structure, the floor function `Nat.floor : α -> Nat` is monotone, i.e., `Nat.floor a <= Nat.floor b` whenever `a <= b` in `α`.
|
Int.le_ceil
theorem Int.le_ceil : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), a ≤ ↑⌈a⌉
This theorem states that for any element 'a' of a certain type 'α', where 'α' is a linearly ordered ring with a flooring operation, the value of 'a' is always less than or equal to the ceiling of 'a'. The ceiling function, denoted as '⌈a⌉', rounds 'a' up to the nearest integer, and the theorem ensures that 'a' will never be larger than this rounded value.
More concisely: For any element 'a' in a linearly ordered ring with a flooring operation, the element 'a' is less than or equal to its ceiling '⌈a⌉'.
|
Nat.floor_div_eq_div
theorem Nat.floor_div_eq_div :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] [inst_1 : FloorSemiring α] (m n : ℕ), ⌊↑m / ↑n⌋₊ = m / n := by
sorry
This theorem states that for any type `α` that is a `LinearOrderedSemifield` and a `FloorSemiring`, and for any natural numbers `m` and `n`, the floor of the division of `m` and `n` when they are cast to `α` is equal to the integer division of `m` and `n`. In mathematical terms, the theorem says that $\left\lfloor\frac{m}{n}\right\rfloor = \frac{m}{n}$ for all natural numbers $m$ and $n$, where $\left\lfloor x \right\rfloor$ denotes the floor function, which rounds $x$ down to the nearest integer.
More concisely: For any natural numbers $m$ and $n$ in a type `α` that is both a LinearOrderedSemifield and a FloorSemiring, $\left\lfloor\frac{m}{n}\right\rfloor = \frac{m}{n}$.
|
Mathlib.Algebra.Order.Floor._auxLemma.3
theorem Mathlib.Algebra.Order.Floor._auxLemma.3 :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
(⌈a⌉₊ ≤ n) = (a ≤ ↑n)
This theorem, from the Mathlib library in Lean 4, states that for any type `α` that has the structure of a linearly ordered semiring and a floor semiring, and for any element `a` of this type and natural number `n`, the property that the ceiling of `a` is less than or equal to `n` is equivalent to the property that `a` itself is less than or equal to the natural number `n` converted to the type `α`. In other words, it explores the relationship between the floor function and the natural ordering on the set.
More concisely: For any linearly ordered semiring `α` with a floor semiring, the ceiling of an element `a` in `α` is less than or equal to a natural number `n` if and only if `a` is less than or equal to the floor of `n` in `α`.
|
Int.ceil_eq_on_Ioc
theorem Int.ceil_eq_on_Ioc :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (z : ℤ), ∀ a ∈ Set.Ioc (↑z - 1) ↑z, ⌈a⌉ = z
The theorem `Int.ceil_eq_on_Ioc` states that for any integer `z` and any element `a` belonging to the set `Set.Ioc` (an interval open on the left and closed on the right), where the interval is between `z - 1` and `z` inclusive (after coercing `z` and `z-1` to the same type as `a`), the ceiling of `a` (`⌈a⌉`) is equal to `z`. This is true in the context of a `LinearOrderedRing` (a ring with a total ordering compatible with ring operations) and a `FloorRing` (a ring with a floor function).
More concisely: For any integer `z` and any `x` in the open interval `(z-1, z]`, the ceiling of `x` equals `z`.
|
Nat.floor_add_nat
theorem Nat.floor_add_nat :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α},
0 ≤ a → ∀ (n : ℕ), ⌊a + ↑n⌋₊ = ⌊a⌋₊ + n
This theorem states that for any non-negative element 'a' of a linear ordered semiring, when you add a natural number 'n' to 'a', the floor of the result is equal to the floor of 'a' added to 'n'. Here, the floor operation is defined on a semiring equipped with a floor operation. It's important to note that the floor function returns the greatest integer less than or equal to a given number, so this theorem is dealing with the interaction of floor operations and addition.
More concisely: For any non-negative element $a$ in a linear ordered semiring with a floor operation, $\lfloor a + n \rfloor = \lfloor a \rfloor + n$.
|
Int.ceil_intCast
theorem Int.ceil_intCast : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (z : ℤ), ⌈↑z⌉ = z := by
sorry
This theorem states that for any integer `z`, when cast to a type `α`, which is a linear ordered ring and a floor ring, the ceiling operation on the cast value will equal the original integer `z`. In essence, the ceiling of an integer, when it's cast to a certain type, is the integer itself.
More concisely: For any integer `z`, the ceiling function of `z` when considered as an element of a linear ordered ring and a floor ring `α` is equal to `z` itself.
|
Nat.le_ceil
theorem Nat.le_ceil : ∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] (a : α), a ≤ ↑⌈a⌉₊
This theorem, `Nat.le_ceil`, states that for any type `α` which forms a linear ordered semiring and has a floor semiring (these are mathematical structures that satisfy certain properties), every element `a` of type `α` is less than or equal to its ceiling. The ceiling of a number, denoted `⌈a⌉₊`, is the smallest integer that is greater than or equal to `a`. Thus, this theorem says that no number is greater than its ceiling, which is a basic property of the ceiling function.
More concisely: For any element `a` of a linear ordered semiring with a floor semiring, `a ≤ ⌈a⌉`.
|
Mathlib.Algebra.Order.Floor._auxLemma.8
theorem Mathlib.Algebra.Order.Floor._auxLemma.8 :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
0 ≤ a → (⌊a⌋₊ < n) = (a < ↑n)
This theorem, from the 'Mathlib.Algebra.Order.Floor' section of Mathlib, states that for any type `α` equipped with the structure of a linearly ordered semiring and a floor semiring, and for any value `a` of type `α` and natural number `n`, the inequality "the floor of `a` is less than `n`" is equivalent to "a is less than the coercion of `n` to type `α`". This is true whenever `a` is non-negative. In simpler terms, if `a` is a non-negative number, then rounding `a` down to the nearest whole number and comparing that to `n` is the same as directly comparing `a` to `n`.
More concisely: For any linearly ordered semiring `α` with a floor semiring, and for any non-negative `α` value `a` and natural number `n`, `floor a < n` if and only if `a < n`.
|
Int.fract_add_nat
theorem Int.fract_add_nat :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (m : ℕ),
Int.fract (a + ↑m) = Int.fract a
The theorem `Int.fract_add_nat` states that for any type `α` that is a linearly ordered ring and a floor ring, for any element `a` of type `α` and any natural number `m`, the fractional part of the sum of `a` and `m` is the same as the fractional part of `a`. In mathematical terms, this can be represented as `fract(a + m) = fract(a)`, where `fract` denotes the fractional part of a number.
More concisely: For any linearly ordered ring and floor ring type `α` and element `a` of `α` and natural number `m`, the fractional part of `a + m` equals the fractional part of `a`.
|
Nat.lt_floor_add_one
theorem Nat.lt_floor_add_one :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] (a : α), a < ↑⌊a⌋₊ + 1
This theorem states that for any given element `a` from a certain type `α` (where `α` is a linearly ordered semiring with a floor semiring structure), `a` is less than the floor of `a` (denoted as `⌊a⌋₊`) incremented by one. This is a common property of floor functions that round down to the nearest integer.
More concisely: For any element `a` in a linearly ordered semiring `α` with a floor semiring structure, `⌊a⌋ + 1 <= a`.
|
Int.gc_coe_floor
theorem Int.gc_coe_floor :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], GaloisConnection Int.cast Int.floor := by
sorry
This theorem states that for any type `α`, if `α` is a `LinearOrderedRing` and a `FloorRing`, then there exists a Galois connection between the function `Int.cast` and `Int.floor`. In other words, the function `Int.cast`, which casts integers to type `α`, and the function `Int.floor`, which maps a number in `α` to the greatest integer less than or equal to it, form a pair of functions that satisfy the property of a Galois connection: for any integer `a` and any number `b` of type `α`, `Int.cast a ≤ b` if and only if `a ≤ Int.floor b`.
More concisely: For any LinearOrderedRing and FloorRing type `α`, the functions `Int.cast` and `Int.floor` form a Galois connection between the integers and `α`, meaning `Int.cast a ≤ b` if and only if `a ≤ Int.floor b`.
|
Int.fract_zero
theorem Int.fract_zero : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], Int.fract 0 = 0 := by
sorry
The theorem `Int.fract_zero` states that for any type `α` that is a linearly ordered ring and has a floor ring structure, the fractional part of the number 0 is 0. In other words, when you subtract the floor (or greatest integer less than or equal to a given number) of 0 from 0, you obtain 0.
More concisely: For any linearly ordered ring with a floor ring structure, the fractional part of 0 is 0.
|
Mathlib.Algebra.Order.Floor._auxLemma.10
theorem Mathlib.Algebra.Order.Floor._auxLemma.10 :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
0 ≤ a → (n ≤ ⌊a⌋₊) = (↑n ≤ a)
This theorem, `Mathlib.Algebra.Order.Floor._auxLemma.10`, from the Mathlib library in Lean 4, states that for any type `α` that is a `LinearOrderedSemiring` and `FloorSemiring`, and for any `a` in `α` and `n` in `ℕ` (the set of natural numbers), provided `a` is non-negative (0 ≤ a), then `n` is less than or equal to the floor of `a` (n ≤ ⌊a⌋₊) if and only if the natural number `n` as a member of `α` (↑n) is less than or equal to `a`. This theorem bridges the relationship between the floor function and basic inequalities in a given ordered semiring.
More concisely: For any `LinearOrderedSemiring` and `FloorSemiring` type `α`, and for all `a : α` non-negative and `n : ℕ`, `n ≤ ⌊a⌋₊ if and only if ↑n ≤ a`.
|
Int.ceil_eq_iff
theorem Int.ceil_eq_iff :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α},
⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z
This theorem, `Int.ceil_eq_iff`, states that for any type `α` which is a linear ordered ring and has a floor function, and any integer `z` and element `a` of type `α`, the ceiling of `a` equals `z` if and only if `a` is strictly greater than `z - 1` and less than or equal to `z`. In mathematical notation, this would be expressed as: if ⌈a⌉ = z, then z - 1 < a ≤ z.
More concisely: For any linear ordered ring `α` with a floor function, `⌈a⌉ = z` if and only if `z - 1 < a <= z`.
|
FloorSemiring.gc_ceil
theorem FloorSemiring.gc_ceil :
∀ {α : Type u_4} [inst : OrderedSemiring α] [self : FloorSemiring α],
GaloisConnection FloorSemiring.ceil Nat.cast
The theorem `FloorSemiring.gc_ceil` states that for any ordered semiring `α` and any floor semiring `α`, the `FloorSemiring.ceil` function, which computes the least natural number `n` such that `a ≤ n` for a given `a` in `α`, forms a Galois connection with the natural number casting function `↑ : ℕ → α`. In other words, for any real number `a` and natural number `b`, `FloorSemiring.ceil a ≤ b` if and only if `a ≤ ↑b`, where `↑` denotes the coercion from natural numbers to `α`. This is the mathematical concept of a lower adjoint in the context of order theory.
More concisely: The `FloorSemiring.ceil` function on an ordered semiring forms a Galois connection with the natural number coercion function, satisfying `FloorSemiring.ceil a ≤ b` if and only if `a ≤ ↑b`.
|
Int.fract_nonneg
theorem Int.fract_nonneg :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), 0 ≤ Int.fract a
The theorem `Int.fract_nonneg` asserts that for any type `α` which is an instance of a `LinearOrderedRing` and a `FloorRing`, the fractional part of any element `a` of this type, as defined by `Int.fract a`, is always non-negative. In other words, the fractional part of a number, obtained by subtracting its floor from it, is always greater than or equal to zero.
More concisely: For any element `a` of a type `α` that is both a LinearOrderedRing and a FloorRing, the fractional part `Int.fract a` of `a` is non-negative.
|
Nat.ceil_one
theorem Nat.ceil_one : ∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α], ⌈1⌉₊ = 1 := by
sorry
This theorem states that for any type `α` which has the properties of a Linear Ordered Semiring and a Floor Semiring, the ceiling function of `1` always equals `1`. In other words, for all these types `α`, the smallest integer that is greater than or equal to `1` is `1` itself. This is generally applicable to any number system that satisfies the properties of a Linear Ordered Semiring and a Floor Semiring.
More concisely: For any type `α` that is both a Linear Ordered Semiring and a Floor Semiring, the ceiling function of `1` equals `1` (i.e., `ceiling 1 = 1`).
|
Int.floor_eq_iff
theorem Int.floor_eq_iff :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α},
⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1
This theorem, named `Int.floor_eq_iff`, states that for all types `α` that are instances of `LinearOrderedRing` and `FloorRing`, and for all integers `z` and any `a` of type `α`, the floor of `a` is equal to `z` if and only if `z` (converted into type `α`) is less than or equal to `a` and `a` is strictly less than `z + 1` (where the integer `z + 1` is converted to type `α`). In mathematical terms, this theorem defines the condition under which the floor function equals a certain integer.
More concisely: For any type `α` instance of `LinearOrderedRing` and `FloorRing`, and for all integers `z` and `α` values `a`, `floor(a) = z` if and only if `z ≤ a` and `a < z + 1` (where `z` and `z + 1` are converted to type `α`).
|
Int.ceil_add_int
theorem Int.ceil_add_int :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (z : ℤ), ⌈a + ↑z⌉ = ⌈a⌉ + z
This theorem states that for any type `α` that has the structure of a `LinearOrderedRing` and a `FloorRing`, and given any element `a` of this type and an integer `z`, the ceiling function of the sum of `a` and `z` (where `z` is treated as an element of `α`) is equal to the sum of the ceiling of `a` and `z`. In mathematical notation, this reads: for all `a` in `α` and `z` in integers (`ℤ`), `⌈a + z⌉ = ⌈a⌉ + z`.
More concisely: For any `LinearOrderedRing` and `FloorRing` type `α`, and for all `a` in `α` and `z` in integers, the ceiling function of `a + z` equals the sum of the ceiling of `a` and `z`. (i.e., `⌈a + z⌉ = ⌈a⌉ + z`)
|
Int.gc_ceil_coe
theorem Int.gc_ceil_coe :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], GaloisConnection Int.ceil Int.cast
The theorem `Int.gc_ceil_coe` states that for all types `α`, where `α` is a linearly ordered ring and also a floor ring, a Galois connection exists between the function `Int.ceil` and the function `Int.cast`. In other words, for every element `a` from the domain of `Int.ceil` and `b` from the domain of `Int.cast`, `Int.ceil a` is less than or equal to `b` if and only if `a` is less than or equal to `Int.cast b`. This links the concepts of ceiling function and integer casting in a context of ordered rings.
More concisely: For all linearly ordered ring and floor ring types `α`, the ceiling function `Int.ceil` and the integer casting function `Int.cast` form a Galois connection, i.e., `Int.ceil a ≤ b` if and only if `a ≤ Int.cast b` for all `a` in the domain of `Int.ceil` and `b` in the domain of `Int.cast`.
|
Int.floor_zero
theorem Int.floor_zero : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], ⌊0⌋ = 0
This theorem states that for any given type `α`, which is a Linear Ordered Ring and also a Floor Ring, the floor of zero is equal to zero. In other words, for any algebraic structure where subtraction and multiplication are defined and it satisfies the properties of an ordered ring along with a floor function, the greatest integer less than or equal to zero is always zero.
More concisely: For any Linear Ordered Ring and Floor Ring `α`, the floor of `0` is equal to `0`.
|
Nat.floor_le
theorem Nat.floor_le :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α}, 0 ≤ a → ↑⌊a⌋₊ ≤ a
This theorem states that, for any type `α` that is a linearly ordered semiring and has a floor semiring structure, and for any non-negative element `a` of type `α`, the floor of `a` is less than or equal to `a`. Here, the floor function `⌊a⌋₊` is a function that rounds `a` down to the nearest whole number. In LaTeX mathematics notation, this is equivalent to saying ∀a ∈ α, 0 ≤ a → ⌊a⌋ ≤ a.
More concisely: For any linearly ordered semiring `α` with a floor semiring structure, the floor function applied to any non-negative element `a` of `α` is less than or equal to `a`: `∀a ∈ α. 0 ≤ a → ⌊a⌋ ≤ a`.
|
Nat.lt_ceil
theorem Nat.lt_ceil :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ}, n < ⌈a⌉₊ ↔ ↑n < a
This theorem, `Nat.lt_ceil`, states that for any type `α` that is a linear ordered semiring and a floor semiring, and given any `α` value `a` and natural number `n`, `n` is less than the ceiling of `a` if and only if the natural number `n` as a member of `α` is less than `a`. In other words, it links the comparison of a natural number with a real number (through its ceiling function), with the comparison of the same natural number (considered as an `α` number) with the original `α` number.
More concisely: For any linear ordered semiring and floor semiring type `α`, and for all `α` values `a` and natural numbers `n`, `n < a` if and only if `n < ceiling a`.
|
Int.fract_eq_iff
theorem Int.fract_eq_iff :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {a b : α},
Int.fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z
The theorem `Int.fract_eq_iff` states that for any type `α` that forms a linear ordered ring and has a floor function, and for any two elements `a` and `b` of `α`, the fractional part of `a` being equal to `b` is equivalent to `b` being greater than or equal to zero and less than one, and there exists an integer `z` such that `a` minus `b` equals to `z`. In mathematical terms, this theorem states that $fract(a) = b$ if and only if $0 \leq b < 1$ and there exists an integer $z$ such that $a - b = z$.
More concisely: The theorem `Int.fract_eq_iff` asserts that for any type `α` with a floor function and ordering, the fractional parts of elements `a` and `b` are equal if and only if `b` is between 0 and 1, and `a` equals `b` plus an integer.
|
FloorRing.gc_coe_floor
theorem FloorRing.gc_coe_floor :
∀ {α : Type u_4} [inst : LinearOrderedRing α] [self : FloorRing α], GaloisConnection Int.cast FloorRing.floor := by
sorry
The theorem `FloorRing.gc_coe_floor` states that for every type `α`, which is a linear ordered ring with a floor function, there exists a Galois connection between the function that casts integers to `α` and the floor function. In other words, for any integer `a` and any element `b` of the type `α`, casting `a` to `α` is less than or equal to `b` if and only if `a` is less than or equal to the floor of `b`. This essentially says that the floor of a number in `α` is the greatest integer less than or equal to that number, and underscores the adjoint relationship between the casting and floor functions.
More concisely: For any linear ordered ring `α` with a floor function, the casting function from integers to `α` forms a Galois connection with the floor function, i.e., for all integers `a` and `α` elements `b`, `a ≤ floor b` if and only if `a ․0 ≤ b`.
|
Nat.floor_zero
theorem Nat.floor_zero : ∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α], ⌊0⌋₊ = 0 := by
sorry
This theorem, `Nat.floor_zero`, states that for all types `α`, if `α` is a linear ordered semiring and a floor semiring, then the floor of zero is zero. In simple mathematical terms, it's saying that the greatest integer less than or equal to zero in any such semiring is indeed zero.
More concisely: For any linear ordered semiring and floor semiring type `α`, the floor of zero is zero.
|
Int.floor_eq_on_Ico
theorem Int.floor_eq_on_Ico :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (n : ℤ),
∀ a ∈ Set.Ico (↑n) (↑n + 1), ⌊a⌋ = n
This theorem states that for any integer `n` and any real number `a` that lies in the left-closed right-open interval from `n` to `n + 1` (denoted as `[n, n+1)`), the floor function of `a` equals `n`. In other words, if `a` is any number in the interval `[n, n+1)` then the greatest integer less than or equal to `a` is `n`.
More concisely: For any integer `n` and real number `a` with `n ≤ a < n+1`, the floor function `⌊a⌋ = n`.
|
Int.floor_lt
theorem Int.floor_lt :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, ⌊a⌋ < z ↔ a < ↑z
This theorem, `Int.floor_lt`, states that for any type `α`, where `α` is a linearly ordered ring and a floor ring, and for any integer `z` and element `a` of type `α`, the floor of `a` is less than `z` if and only if `a` is less than the coercion of `z` to type `α`. In mathematical terms, it can be expressed as: if `⌊a⌋ < z` then `a < ↑z`, and if `a < ↑z` then `⌊a⌋ < z`.
More concisely: For any linearly ordered ring and floor ring `α`, and for all `z` an integer and `a` an element of `α`, `⌊a⌋ < z` if and only if `a < ↑z`.
|
Nat.le_floor
theorem Nat.le_floor :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ}, ↑n ≤ a → n ≤ ⌊a⌋₊
This theorem, `Nat.le_floor`, states that for any type `α` which is a linear ordered semiring and also a floor semiring, and any elements `a` of type `α` and `n` of type natural numbers (`ℕ`), if `n` is less than or equal to `a` (when `n` is coerced to type `α`), then `n` is less than or equal to the nonnegative floor of `a`. In simpler terms, if a natural number `n` is not greater than a real number `a`, then `n` is not greater than the greatest whole number less than or equal to `a`.
More concisely: For any linear ordered semiring and floor semiring type `α`, and any `a` of type `α` and natural number `n`, if `n ≤ a` then `n ≤ floor a`, where `floor` is the nonnegative floor function.
|
subsingleton_floorSemiring
theorem subsingleton_floorSemiring :
∀ {α : Type u_4} [inst : LinearOrderedSemiring α], Subsingleton (FloorSemiring α)
This theorem states that for any linear ordered semiring of a certain type α, there can exist at most one `FloorSemiring` structure. In other words, the `FloorSemiring` structure is unique for a given linear ordered semiring. This is a characteristic of the mathematical concept of floor semirings in the context of linear ordered semirings.
More concisely: For any linear ordered semiring α, there exists at most one FloorSemiring structure.
|
Nat.floor_lt
theorem Nat.floor_lt :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
0 ≤ a → (⌊a⌋₊ < n ↔ a < ↑n)
This theorem states that for any type `α` that is a linear ordered semiring and a floor semiring, for any instance `a` of that type `α` and any natural number `n`, if `a` is greater than or equal to zero, then the floor of `a` is less than `n` if and only if `a` is less than the conversion of `n` to the type `α`. In other words, it establishes an equivalence between the comparison of the floor of a non-negative number `a` with a natural number `n` and the comparison of `a` itself with `n` in the context of the type `α`.
More concisely: For any linear ordered semiring and floor semiring type `α`, with `a : α` non-negative, the floor of `a` is less than a natural number `n` if and only if `a` is strictly less than the conversion of `n` to `α`.
|
Mathlib.Algebra.Order.Floor._auxLemma.35
theorem Mathlib.Algebra.Order.Floor._auxLemma.35 :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, (⌊a⌋ < z) = (a < ↑z) := by
sorry
This theorem, `Mathlib.Algebra.Order.Floor._auxLemma.35`, states that for any type `α` that is a linearly ordered ring and has a floor function, and for any integer `z` and any element `a` of `α`, the inequality `⌊a⌋ < z` (the floor of `a` is less than `z`) is equivalent to the inequality `a < ↑z` ( `a` is less than the integer `z` coverted to `α`).
More concisely: For any linearly ordered ring `α` with a floor function, the inequality `⌊a⌋ < z` is equivalent to `a < ↑z`.
|
Nat.floor_coe
theorem Nat.floor_coe :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] (n : ℕ), ⌊↑n⌋₊ = n
This theorem, `Nat.floor_coe`, states that for any natural number `n`, the floor function applied to the associated number in a linear ordered semiring `α` results in `n` itself. In other words, if we take a natural number `n`, cast it into some type `α` where `α` is a linearly ordered semiring that also supports a floor operation, and then apply the floor operation, we get the original natural number `n` back. This property holds for all natural numbers and any type `α` satisfying these conditions.
More concisely: For any natural number `n` and any linearly ordered semiring `α` with a floor operation, `floor (alg_num n) = n`, where `alg_num` is the function that casts natural numbers to `α`.
|
Int.fract_pos
theorem Int.fract_pos :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {a : α}, 0 < Int.fract a ↔ a ≠ ↑⌊a⌋
The theorem `Int.fract_pos` states that for any number `a` of a type `α` that forms a linear ordered ring and has a floor function, the fractional part of `a`, represented as `Int.fract a`, is positive if and only if `a` is not equal to its floor, denoted as `⌊a⌋`. In other words, a number has a positive fractional part exactly when the number is not an integer.
More concisely: The theorem `Int.fract_pos` asserts that the fractional part of a number `a` in a lined ordered ring with a floor function is positive if and only if `a` is not an integer.
|
Nat.le_floor_iff'
theorem Nat.le_floor_iff' :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
n ≠ 0 → (n ≤ ⌊a⌋₊ ↔ ↑n ≤ a)
This theorem states that for any type `α` that forms a linear ordered semiring and a floor semiring, and for any non-zero natural number `n` and any element `a` of type `α`, the statement "n is less than or equal to the floor of a" is equivalent to "n as an element of the semiring is less than or equal to a". This theorem is useful for performing comparisons involving the floor function in a semiring.
More concisely: For any linear ordered semiring `α` and non-zero natural number `n` in `α`, the equality `n ≤ floor a` holds if and only if `n` is less than or equal to `a` in the semiring `α`.
|
Mathlib.Algebra.Order.Floor._auxLemma.9
theorem Mathlib.Algebra.Order.Floor._auxLemma.9 :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
(n < ⌈a⌉₊) = (↑n < a)
This theorem, from the Mathlib algebraic order and floor functions library in Lean 4, states that for any type `α` that is a linear ordered semiring and a floor semiring, and for any `α` value `a` and natural number `n`, the inequality `n` is less than the ceiling of `a` is equivalent to the inequality that the real number representation of `n` is less than `a`. The ceiling function `⌈a⌉₊` rounds `a` up to the nearest whole number, while `↑n` denotes the real number representation of `n`.
More concisely: For any linear ordered semiring and floor semiring type `α` and values `a` of type `α` and `n` of type `nat`, `n < ⌈a⌉` if and only if `↑n < a`.
|
Nat.floor_of_nonpos
theorem Nat.floor_of_nonpos :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α}, a ≤ 0 → ⌊a⌋₊ = 0
This theorem states that for any type `α` that has a `LinearOrderedSemiring` and `FloorSemiring` structure, if a variable `a` of type `α` is less than or equal to zero, then the floor of `a` in the context of natural numbers (denoted by `⌊a⌋₊`) is equal to zero. In mathematical terms, this means that for any real number `a` less than or equal to zero, when you round `a` down to the nearest whole number, the result is zero.
More concisely: For any type `α` with `LinearOrderedSemiring` and `FloorSemiring` structures, if `α` has a negative or zero element, then `⌊x⌋₊ = 0` for all `x : α` in that type.
|
subsingleton_floorRing
theorem subsingleton_floorRing : ∀ {α : Type u_4} [inst : LinearOrderedRing α], Subsingleton (FloorRing α)
This theorem states that for any given type `α` that has a structure of a linear ordered ring, there can be at most one `FloorRing` structure on `α`. In other words, the `FloorRing` structure on any linear ordered ring `α` is unique, if it exists.
More concisely: For any linear ordered ring `α`, there exists at most one `FloorRing` structure on it.
|
Int.floor_intCast
theorem Int.floor_intCast : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (z : ℤ), ⌊↑z⌋ = z := by
sorry
The theorem `Int.floor_intCast` states that for any integer `z`, when it is cast into a type `α` (which is assumed to be a linearly ordered ring and a floor ring), the floor function applied to the cast value equals `z`. In simpler terms, the theorem states that when you take an integer, turn it into a decimal number and then round down to the nearest integer, you'll end up with the original integer.
More concisely: For any integer `z` and any linearly ordered ring `α`, the floor function applied to the cast of `z` to `α` equals `z`.
|
FloorRing.gc_ceil_coe
theorem FloorRing.gc_ceil_coe :
∀ {α : Type u_4} [inst : LinearOrderedRing α] [self : FloorRing α], GaloisConnection FloorRing.ceil Int.cast := by
sorry
This theorem states that for any type `α` that is a linear ordered ring and has a `FloorRing` structure, the function `FloorRing.ceil`, which computes the smallest integer greater than or equal to a given element of `α`, is the lower adjoint of the function that coerces integers to elements of `α`. In other words, for any elements `a` of `α` and `b` of `ℤ`, the property `FloorRing.ceil a ≤ b` holds if and only if `a ≤ Int.cast b`. This is an application of the Galois Connection concept in order theory.
More concisely: The function `FloorRing.ceil` on a linear ordered ring `α` with a `FloorRing` structure is the lower adjoint of the integer coercion function, i.e., for all `a` in `α` and `b` in `ℤ`, `FloorRing.ceil a ≤ b` if and only if `a ≤ Int.cast b`.
|
Int.fract_add_int
theorem Int.fract_add_int :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (m : ℤ),
Int.fract (a + ↑m) = Int.fract a
The theorem `Int.fract_add_int` states that for any type `α` that forms a linear ordered ring and has a floor ring structure, and for any elements `a` of `α` and `m` of the integers (`ℤ`), the fractional part of `a` plus `m` (i.e., `a + m`) is the same as the fractional part of `a`. In mathematical terms, if `fract(x)` represents the fractional part of `x`, this theorem is saying that `fract(a + m) = fract(a)` for all such `a` and integer `m`.
More concisely: For any element `a` in a linear ordered ring with a floor ring structure and any integer `m`, the fractional parts of `a` and `a + m` are equal.
|
Nat.sub_one_lt_floor
theorem Nat.sub_one_lt_floor :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorSemiring α] (a : α), a - 1 < ↑⌊a⌋₊
This theorem states that for any type `α`, given that `α` is a linearly ordered ring and a floor semiring, the value of any element `a` of type `α` subtracted by 1 is less than the floor of `a` coerced to `α`. In mathematical terms, for any `a` in a linearly ordered ring and floor semiring `α`, `a - 1 < floor(a)`.
More concisely: For any linearly ordered ring and floor semiring `α`, the floor function applied to any element `a` in `α` is strictly greater than `a - 1`. In Lean 4 notation: `floor a > a - 1`.
|
Mathlib.Algebra.Order.Floor._auxLemma.37
theorem Mathlib.Algebra.Order.Floor._auxLemma.37 :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, (⌈a⌉ ≤ z) = (a ≤ ↑z) := by
sorry
This theorem, from the Mathlib library in Lean 4, states that for any type `α` that is a linear ordered ring and a floor ring, and for any integer `z` and any value `a` of type `α`, the statement that the ceiling of `a` is less than or equal to `z` is equivalent to the statement that `a` is less than or equal to the real number equivalent of `z`. In other words, it shows that, in the context of certain mathematical structures, comparing a number to the ceiling of another number is the same as comparing it to the other number itself.
More concisely: For any linear ordered ring and floor ring type `α`, and integers `z` and `a` of type `α`, `a <= toReal z` if and only if `ceiling a <= z`.
|
Int.floor_natCast
theorem Int.floor_natCast : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (n : ℕ), ⌊↑n⌋ = ↑n
This theorem, `Int.floor_natCast`, states that for any natural number `n` in a linear ordered ring `α` that also has a floor function, the floor of the natural number `n` when cast to `α` is equal to `n` when cast to `α`. Essentially, it shows that the floor function of a natural number, after type casting, retains the original value.
More concisely: For any natural number `n` in a linear ordered ring with a floor function, `α`, the floor of `n` cast to `α` equals the cast of `n` to `α`. In Lean syntax: `(∀ (α : Type u) [LinearOrderedAddCommMonoid α] [HasFloor α], ∀ (n : ℕ), floor α (coe n) = coe n)`.
|
Int.le_floor
theorem Int.le_floor :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, z ≤ ⌊a⌋ ↔ ↑z ≤ a
This theorem, `Int.le_floor`, states that for any type `α` which forms a linearly ordered ring and has a floor function, and for any integer `z` and element `a` of type `α`, the integer `z` is less than or equal to the floor of `a` if and only if the real number representation of `z` is less than or equal to `a`. In other words, it establishes the equivalence between the inequality of an integer and the floor of a real number, and the inequality of the real representations of those numbers.
More concisely: For any linearly ordered ring type `α` with a floor function, the integer `z` is less than or equal to the floor of the element `a` of type `α` if and only if the real number representation of `z` is less than or equal to `a`.
|
Int.fract_intCast
theorem Int.fract_intCast :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (z : ℤ), Int.fract ↑z = 0
This theorem states that for any integer `z`, when `z` is cast to a type `α` that is a linearly ordered ring with a floor function, the fractional part of `z` is zero. In other words, the fractional part of any integer, when the integer is considered as an element of a linearly ordered ring with a floor function, is always zero. This is expressed mathematically as `Int.fract ↑z = 0` for all integers `z`.
More concisely: For any integer `z`, the fractional part of `z` in a linearly ordered ring with a floor function is zero. In symbols, `Int.fract (Floor z) = 0` for all integers `z`.
|
Nat.ceil_natCast
theorem Nat.ceil_natCast :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] (n : ℕ), ⌈↑n⌉₊ = n
This theorem, `Nat.ceil_natCast`, states that for any natural number `n`, when this number is cast to a type `α` (which is a linear ordered semiring and a floor semiring), and we take the ceiling of this value, we will always get back `n`. In other words, the ceiling of a natural number, when it is considered as a real number, is just the number itself.
More concisely: For any natural number `n` and any linear ordered semiring and floor semiring type `α`, the ceiling of `n` cast to `α` is equal to `n`.
|
Mathlib.Algebra.Order.Floor._auxLemma.38
theorem Mathlib.Algebra.Order.Floor._auxLemma.38 :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] {z : ℤ} {a : α}, (z ≤ ⌊a⌋) = (↑z ≤ a) := by
sorry
This theorem, from the `Mathlib.Algebra.Order.Floor` library, is known as `_auxLemma.38`. It asserts that for any integer `z` and any element `a` of a type `α`, where `α` is a linearly ordered ring with a floor function, `z` is less than or equal to the floor of `a` if and only if the real number equivalent of `z` is less than or equal to `a`. In other words, the comparison of an integer `z` with the floor of a number `a` in this ordered ring structure is equivalent to the comparison of the real number variant of `z` with `a`. This theorem provides a useful equivalence relation that bridges the gap between integers and reals in the context of linearly ordered rings with a floor function.
More concisely: For any integer `z` and element `a` in a linearly ordered ring with a floor function, `z ≤ floor a` if and only if `reál z ≤ a`.
|
Nat.ceil_le
theorem Nat.ceil_le :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ}, ⌈a⌉₊ ≤ n ↔ a ≤ ↑n
This theorem, `Nat.ceil_le`, states that for any type `α` which is a Linear Ordered Semiring and a Floor Semiring, and for any `a` of type `α` and natural number `n`, the ceiling of `a` (denoted as `⌈a⌉₊`) is less than or equal to `n` if and only if `a` is less than or equal to the natural number representation of `n` (`↑n`). In other words, the ceiling of `a` is less than or equal to `n` precisely when `a` itself is less than or equal to `n` when `n` is considered as a member of type `α`.
More concisely: For any Linear Ordered Semiring and Floor Semiring type `α`, and for all `a` in `α` and natural number `n`, `⌈a⌉₊ ≤ n` if and only if `a ≤ ↑n`.
|
Int.ceil_mono
theorem Int.ceil_mono : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], Monotone Int.ceil := by
sorry
The theorem `Int.ceil_mono` asserts that for any type `α` that is a `LinearOrderedRing` and a `FloorRing`, the function `Int.ceil` is monotone. This means, given any two real numbers `a` and `b` such that `a ≤ b`, the smallest integer greater than or equal to `a` is less than or equal to the smallest integer greater than or equal to `b`. In other words, if `a` is less than or equal to `b`, then `⌈a⌉` is less than or equal to `⌈b⌉`.
More concisely: For any type `α` that is a LinearOrderedRing and a FloorRing, the ceiling function `⌈.⌉ : ℝ → ℤ` is a monotone function, i.e., `a ≤ b` implies `⌈a⌉ ≤ ⌈b⌉`.
|
Int.ceil_lt_add_one
theorem Int.ceil_lt_add_one :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), ↑⌈a⌉ < a + 1
This theorem, `Int.ceil_lt_add_one`, states that for any element `a` of a certain type `α`, the ceiling of `a` (i.e., the smallest integer not smaller than `a`) is strictly less than `a + 1`. Here, `α` is a type that forms a linear ordered ring with an associated floor ring structure. In mathematical terms, it is saying that for all `a` in a floor ring, the inequality $\lceil a \rceil < a + 1$ holds.
More concisely: For all elements `a` in a floor ring, the ceiling of `a` is strictly less than `a + 1`.
|
Int.fract_lt_one
theorem Int.fract_lt_one :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), Int.fract a < 1
The theorem `Int.fract_lt_one` states that for any value `a` in a type `α` that forms a linear ordered ring with a floor function, the fractional part of `a` (which is defined as `a` minus its floor) is always less than 1.
More concisely: For any element `a` in a linear ordered ring with a floor function, the value of the fractional part `a - floor a` is less than 1.
|
Nat.le_floor_iff
theorem Nat.le_floor_iff :
∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α] {a : α} {n : ℕ},
0 ≤ a → (n ≤ ⌊a⌋₊ ↔ ↑n ≤ a)
This theorem, `Nat.le_floor_iff`, states that for any type `α` that is a linear ordered semiring and has a floor semiring structure, and given any `α` value `a` that is non-negative, and any natural number `n`, `n` is less than or equal to the floor of `a` if and only if `n` when promoted to `α` is less than or equal to `a`. In other words, a natural number `n` is less than or equal to the floor of a non-negative real number `a` if and only if `n` as a real number is less than or equal to `a`.
More concisely: For any non-negative real number `a` and natural number `n`, `n ≤ floor a` if and only if `n ≤ a` as real numbers.
|
Int.floor_sub_nat
theorem Int.floor_sub_nat :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α) (n : ℕ), ⌊a - ↑n⌋ = ⌊a⌋ - ↑n := by
sorry
This theorem states that for any type `α` that is a LinearOrderedRing and has a FloorRing structure, and for any element `a` of type `α` and natural number `n`, the floor of the difference between `a` and `n` (`⌊a - ↑n⌋`) is equal to the difference between the floor of `a` and `n` (`⌊a⌋ - ↑n`). In other words, subtracting a natural number from a value before taking the floor yields the same result as first taking the floor of the value and then subtracting the natural number.
More concisely: For any LinearOrderedRing `α` with a FloorRing structure and any `a` in `α` and natural number `n`, `⌊a - ↑n⌋ = ⌊a⌋ - n`.
|
Int.floor_one
theorem Int.floor_one : ∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α], ⌊1⌋ = 1
This theorem states that for any type `α` that is a linear ordered ring and a floor ring, the floor value of `1` is `1`. In mathematical terms, this theorem asserts that for any `α` in the categories of linear ordered rings and floor rings, applying the floor function to `1` will always yield `1`.
More concisely: For any type `α` that is both a linear ordered ring and a floor ring, the floor function of `1` is equal to `1`.
|
Nat.floor_one
theorem Nat.floor_one : ∀ {α : Type u_2} [inst : LinearOrderedSemiring α] [inst_1 : FloorSemiring α], ⌊1⌋₊ = 1 := by
sorry
This theorem, `Nat.floor_one`, states that for any type `α` that is a `LinearOrderedSemiring` and a `FloorSemiring`, the floor function applied to the number one (`1`) is equal to one (`1`). In other words, it's saying that the greatest integer less than or equal to one is one itself, which is obviously true as one is an integer.
More concisely: For any type `α` that is both a LinearOrderedSemiring and a FloorSemiring, the floor function of 1 equals 1.
|
FloorSemiring.gc_floor
theorem FloorSemiring.gc_floor :
∀ {α : Type u_4} [inst : OrderedSemiring α] [self : FloorSemiring α] {a : α} {n : ℕ},
0 ≤ a → (n ≤ FloorSemiring.floor a ↔ ↑n ≤ a)
The theorem `FloorSemiring.gc_floor` states that for any ordered semiring `α`, any element `a` of `α` such that `0` is less than or equal to `a`, and any natural number `n`, `n` is less than or equal to the floor of `a` if and only if the natural number `n` when casted as an element of `α` is less than or equal to `a`. In other words, it's asserting the connection between the natural number domain and the ordered semiring domain in the context of the floor function.
More concisely: For any ordered semiring `α` and elements `a` in `α` with `0 ≤ a`, the natural number `n` is less than or equal to the floor of `a` if and only if the cast of `n` to `α` is less than or equal to `a`.
|
Int.lt_floor_add_one
theorem Int.lt_floor_add_one :
∀ {α : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] (a : α), a < ↑⌊a⌋ + 1
This theorem states that for any type `α` that is a linearly ordered ring and also a floor ring, any element `a` of type `α` is strictly less than the floor of `a` (denoted as ⌊a⌋) plus one. In other words, for any real number `a`, `a` is less than its floor value incremented by one.
More concisely: For any linearly ordered ring and floor ring type `α`, and any `a` of type `α`, `a` is strictly less than the floor of `a` plus one.
|