Mathlib.Algebra.Order.Archimedean._auxLemma.2
theorem Mathlib.Algebra.Order.Archimedean._auxLemma.2 :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
(a - b < c) = (a < b + c)
This theorem states that for any type `α`, if `α` is an additive commutative group and has an order (`<`) that is covariant with respect to addition, then for any elements `a`, `b`, and `c` of `α`, the statement "the difference of `a` and `b` is less than `c`" is equivalent to the statement " `a` is less than the sum of `b` and `c`". This provides a kind of distributive property for the less-than relation over subtraction and addition.
More concisely: For any additive commutative group `α` with covariant order `<`, the relation `a < b => a + c < b + c` holds for all `a, b, c ∈ α`.
|
le_of_forall_lt_rat_imp_le
theorem le_of_forall_lt_rat_imp_le :
∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : Archimedean α] {x y : α},
(∀ (q : ℚ), y < ↑q → x ≤ ↑q) → x ≤ y
This theorem states that for any type `α` that is a linear ordered field and is archimedean, if for every rational number `q` the property holds that whenever `y` is less than `q`, `x` is less or equal to `q`, then it follows that `x` is less or equal to `y`. This is essentially a property about the order relationship between `x` and `y` in the context of any rational number `q`.
More concisely: For any archimedean linear ordered field `α`, if `x ≤ q` and `y < q` imply `x ≤ y`, then `α` is total ordered.
|
existsUnique_zsmul_near_of_pos
theorem existsUnique_zsmul_near_of_pos :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α] {a : α},
0 < a → ∀ (g : α), ∃! k, k • a ≤ g ∧ g < (k + 1) • a
This theorem states that in any Archimedean decidable linearly ordered additive commutative group, if we have a positive element `a`, then for any element `g` in the group, there exists a unique integer `k` such that `g` lies between `k` times `a` and `(k + 1)` times `a`. In other words, we can find a unique `k` that "scales" `a` to just below `g`, but not exceeding it. This is essentially a version of the floor function for such groups.
More concisely: In any Archimedean decidable linearly ordered additive commutative group, for each positive element `a` and any group element `g`, there exists a unique integer `k` such that `k * a ≤ g` and `(k + 1) * a > g`.
|
exists_nat_pow_near
theorem exists_nat_pow_near :
∀ {α : Type u_1} [inst : LinearOrderedSemiring α] [inst_1 : Archimedean α] [inst_2 : ExistsAddOfLE α] {x y : α},
1 ≤ x → 1 < y → ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
This theorem states that for any type `α` that is a linearly ordered semiring and which has the Archimedean property and the ability to add elements, given any `x` and `y` of type `α` such that `x` is greater than or equal to 1 and `y` is greater than 1, there exists a natural number `n` such that `y` to the power `n` is less than or equal to `x` and `x` is less than `y` to the power `n + 1`. In other words, every number greater than or equal to 1 can be found between two successive natural-number powers of any number greater than one.
More concisely: For any linearly ordered semiring `α` with the Archimedean property, there exists a natural number `n` such that $1 \leq x < y^n$ holds for all $x, y \in \alpha$ with $x \geq 1$ and $y > 1$.
|
exists_int_lt
theorem exists_int_lt : ∀ {α : Type u_1} [inst : StrictOrderedRing α] [inst_1 : Archimedean α] (x : α), ∃ n, ↑n < x
This theorem, `exists_int_lt`, states that for any type `α` that is a strictly ordered ring and also Archimedean, for any element `x` of that type, there exists an integer `n` such that `n` is less than `x`. In other words, in any Archimedean strictly ordered ring, given any element, we can always find an integer that is less than that element.
More concisely: In any Archimedean strictly ordered ring, every element has a strictly positive integer lower bound.
|
exists_rat_btwn
theorem exists_rat_btwn :
∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : Archimedean α] {x y : α}, x < y → ∃ q, x < ↑q ∧ ↑q < y
This theorem states that for any given type `α` that has an instance of a Linear Ordered Field and Archimedean property, and for any two elements `x` and `y` of this type such that `x` is less than `y`, there exists a rational number `q` such that `q` is greater than `x` and less than `y`. Essentially, it asserts that there's always a rational number between any two distinct elements of a type that behaves as a linearly ordered field and that also has the Archimedean property.
More concisely: For any linearly ordered field `α` with the Archimedean property, given `x` and `y` in `α` with `x < y`, there exists a rational number `q` such that `x < q < y`.
|
exists_pow_lt_of_lt_one
theorem exists_pow_lt_of_lt_one :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] [inst_1 : Archimedean α] [inst_2 : ExistsAddOfLE α] {x y : α},
0 < x → y < 1 → ∃ n, y ^ n < x
This theorem states that for any number `y` less than one and any positive number `x` in a Linear Ordered Semifield that satisfies the Archimedean property and the existence of addition operation, there exists a natural number `n` such that `y` raised to the power of `n` is less than `x`. In mathematical terms, for every `y < 1` and `x > 0`, there exists an `n ∈ ℕ` such that `y^n < x`.
More concisely: For any `y` with `0 < x < 1` in an Archimedean Linear Ordered Semifield, there exists a natural number `n` such that `y^n < x`.
|
exists_rat_gt
theorem exists_rat_gt : ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : Archimedean α] (x : α), ∃ q, x < ↑q
This theorem, `exists_rat_gt`, states that for any given number `x` of a type `α`, where `α` is a linearly ordered field with the Archimedean property, there exists a rational number `q` such that `x` is less than `q`. In other words, for any number in an Archimedean field, you can always find a rational number that is greater than it.
More concisely: For any number `x` in an Archimedean field `α`, there exists a rational number `q` such that `x` < `q`.
|
exists_nat_ge
theorem exists_nat_ge : ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Archimedean α] (x : α), ∃ n, x ≤ ↑n := by
sorry
This theorem, `exists_nat_ge`, states that for any type `α` that is an ordered semiring and is Archimedean (meaning that there are no infinitely small positive numbers), given any element `x` of type `α`, there exists a natural number `n` such that `x` is less than or equal to `n`. In simpler terms, it says that any number in an Archimedean ordered semiring is either less than or equal to some natural number.
More concisely: In any Archimedean ordered semiring, every element is less than or equal to some natural number.
|
pow_unbounded_of_one_lt
theorem pow_unbounded_of_one_lt :
∀ {α : Type u_1} [inst : StrictOrderedSemiring α] [inst_1 : Archimedean α] {y : α} [inst_2 : ExistsAddOfLE α]
(x : α), 1 < y → ∃ n, x < y ^ n
This theorem states that for any strictly ordered semiring `α` with an Archimedean property and a certain `x` in `α`, if `y` is an element of `α` that is greater than `1`, then there exists a natural number `n` such that `x` is less than `y` raised to the power of `n`. Essentially, the power of any number greater than `1` can become arbitrarily large in a strictly ordered semiring, surpassing any given number in the semiring.
More concisely: For any strictly ordered semiring with the Archimedean property and element `x`, there exists a natural number `n` such that `x` is strictly less than `y^n` for `y` being any element greater than 1.
|
exists_int_gt
theorem exists_int_gt : ∀ {α : Type u_1} [inst : StrictOrderedRing α] [inst_1 : Archimedean α] (x : α), ∃ n, x < ↑n
This theorem, named `exists_int_gt`, states that for any type `α` that forms a strictly ordered ring and is Archimedean, given any element `x` of that type, there exists an integer `n` such that `x` is less than `n`. In other words, in any Archimedean strictly ordered ring, any given element is exceeded by some integer.
More concisely: In any Archimedean strictly ordered ring, every element is surpassed by some integer.
|
exists_nat_pow_near_of_lt_one
theorem exists_nat_pow_near_of_lt_one :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] [inst_1 : Archimedean α] [inst_2 : ExistsAddOfLE α] {x y : α},
0 < x → x ≤ 1 → 0 < y → y < 1 → ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
This theorem states that for every type `α`, which is a linear ordered semifield and Archimedean, and for which addition is defined, if `x` and `y` are elements of `α` and are both between `0` and `1`, then there exists a natural number `n` such that `x` is between `y` raised to the power `n + 1` and `y` raised to the power `n`. In more simple terms, for any two numbers `x` and `y` in the range `(0, 1]`, `x` can be placed between two consecutive powers of `y`.
More concisely: For every Archimedean linear ordered semifield `α` with defined addition, and for all `x, y ∈ α` such that `0 < x, y ≤ 1`, there exists a natural number `n` with `x ≤ y^(n+1) ≤ y^n`.
|
add_one_pow_unbounded_of_pos
theorem add_one_pow_unbounded_of_pos :
∀ {α : Type u_1} [inst : StrictOrderedSemiring α] [inst_1 : Archimedean α] {y : α} (x : α),
0 < y → ∃ n, x < (y + 1) ^ n
This theorem states that for any strictly ordered semiring (a mathematical system that is an algebraic structure which generalizes the arithmetic of natural numbers, integers, and real numbers) with the Archimedean property (which states that given any number, there is a natural number that is higher than it), and given any positive number `y`, there exists a natural number `n` such that any number `x` is less than `(y + 1)^n`. This essentially implies that `(y + 1)^n` grows without bound for any positive `y`.
More concisely: For any strictly ordered semiring with the Archimedean property, given a positive element `y`, there exists a natural number `n` such that `(y + 1) ^ n > x` for all positive elements `x`.
|
existsUnique_add_zsmul_mem_Ioc
theorem existsUnique_add_zsmul_mem_Ioc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α] {a : α},
0 < a → ∀ (b c : α), ∃! m, b + m • a ∈ Set.Ioc c (c + a)
This theorem, `existsUnique_add_zsmul_mem_Ioc`, states that for any type `α` which forms a linear ordered additive commutative group and is Archimedean, given any element `a` of that type such that `0 < a`, for any two elements `b` and `c` of that type, there exists a unique integer `m` such that `b + m • a` lies in the left-open right-closed interval from `c` to `c + a`. This means that by multiplying `a` by some integer `m` and adding the result to `b`, we end up with a value that is strictly greater than `c` and less than or equal to `c + a`.
More concisely: For any Archimedean additive commutative group type `α` with a positive element `a`, and for all `b` and `c` in `α` with `0 < a` and `c < b`, there exists a unique integer `m` such that `b + m*a ∈ (c, c + a]`.
|
existsUnique_zsmul_near_of_pos'
theorem existsUnique_zsmul_near_of_pos' :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α] {a : α},
0 < a → ∀ (g : α), ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
This theorem states that for any type `α` that forms a linear ordered additive commutative group and satisfies the Archimedean property, and for any element `a` of type `α` that is greater than zero, for every element `g` of type `α`, there exists a unique integer `k` such that the difference `g - k•a` is non-negative and less than `a`. Here, `k•a` represents the operation of multiplying `a` by `k` times in the group. The Archimedean property essentially states that there are no infinitely small or infinitely large elements in the group.
More concisely: For any Archimedean, linearly ordered additive commutative group `α` and positive element `a` in `α`, there exists a unique integer `k` such that `g - k•a` is non-negative and less than `a`, for all `g` in `α`.
|
archimedean_iff_nat_lt
theorem archimedean_iff_nat_lt :
∀ {α : Type u_1} [inst : LinearOrderedField α], Archimedean α ↔ ∀ (x : α), ∃ n, x < ↑n
This theorem, named `archimedean_iff_nat_lt`, states that for any type `α` that is a linearly ordered field, the property of being Archimedean is equivalent to a property that, for any element `x` of type `α`, there exists a natural number `n` such that `x` is less than the natural number `n`. In terms of mathematics, a field is called Archimedean if for every element in the field, there exists a natural number greater than that element.
More concisely: A linearly ordered field is Archimedean if and only if for every element x in the field, there exists a natural number n such that x < n.
|
Archimedean.arch
theorem Archimedean.arch :
∀ {α : Type u_2} [inst : OrderedAddCommMonoid α] [self : Archimedean α] (x : α) {y : α}, 0 < y → ∃ n, x ≤ n • y
This theorem, named `Archimedean.arch`, states that for any type `α` which is an ordered additive commutative monoid and also satisfies the Archimedean property, and for any two elements `x` and `y` in `α` such that `y` is greater than zero, there exists a natural number `n` such that `x` is less than or equal to `n` times `y`.
In other words, this is a formalization of the Archimedean property, which in the context of numbers is the principle that given any number, no matter how large, and any positive number, no matter how small, there is a multiple of the smaller number that is larger than the larger number.
More concisely: For any ordered additive commutative monoid `α` with the Archimedean property, given `x, y ∈ α` with `y > 0`, there exists a natural number `n` such that `x ≤ n * y`.
|
exists_nat_gt
theorem exists_nat_gt :
∀ {α : Type u_1} [inst : StrictOrderedSemiring α] [inst_1 : Archimedean α] (x : α), ∃ n, x < ↑n
This theorem states that for any value `x` of a type `α`, there exists a natural number `n` such that `x` is less than `n`. Here, `α` is a type that forms a strictly ordered semiring and also satisfies the Archimedean property. The Archimedean property is a property of ordered or normed fields and rings, which roughly states that there are no infinitesimally small or infinitely large elements. In a more concrete sense, given an arbitrary element `x`, you can always find a natural number `n` that is greater than `x`, which is the essence of this theorem.
More concisely: For any element `x` in a type `α` that forms a strictly ordered semiring and satisfies the Archimedean property, there exists a natural number `n` such that `x` is less than `n`.
|
exists_rat_lt
theorem exists_rat_lt : ∀ {α : Type u_1} [inst : LinearOrderedField α] [inst_1 : Archimedean α] (x : α), ∃ q, ↑q < x
This theorem states that for any type `α` that has the structure of a linear ordered field and is Archimedean, given any element `x` of this type, there exists a rational number `q` such that `q` is less than `x`. In mathematical terms, this theorem asserts that for any real number `x`, there is always a rational number `q` such that `q < x`. It's an embodiment of the fact that the rational numbers are dense in the real numbers.
More concisely: For any Archimedean linear ordered field `α`, given any element `x` in `α`, there exists a rational number `q` such that `q < x`.
|
exists_mem_Ico_zpow
theorem exists_mem_Ico_zpow :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] [inst_1 : Archimedean α] [inst_2 : ExistsAddOfLE α] {x y : α},
0 < x → 1 < y → ∃ n, x ∈ Set.Ico (y ^ n) (y ^ (n + 1))
This theorem states that for any positive real number `x` and another real number `y` greater than one, there exists an integer `n` such that `x` is in the left-closed right-open interval between `y` to the power of `n` and `y` to the power of `n + 1`. This is equivalent to saying that any positive real number `x` lies between two consecutive integer powers of any other real number `y` that is greater than one. The theorem relies on the properties of a linear ordered semifield and the Archimedean property of the real numbers, which guarantees the existence of such an `n`.
More concisely: For any positive real number `x` and `y` > 1, there exists an integer `n` such that `y^n` ≤ `x` < `y^(n+1)`.
|
exists_mem_Ioc_zpow
theorem exists_mem_Ioc_zpow :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] [inst_1 : Archimedean α] [inst_2 : ExistsAddOfLE α] {x y : α},
0 < x → 1 < y → ∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
This theorem states that for every positive number 'x' and another number 'y' greater than one, there exists an integer 'n' such that 'x' lies in the interval between 'y' raised to the power of 'n' and 'y' raised to the power of 'n+1'. This interval is open on the left (meaning it does not include 'y' to the power 'n') and closed on the right (meaning it does include 'y' to the power 'n+1'). The theorem applies under the conditions that the type 'α' is a linear ordered semifield, is Archimedean, and supports the operation of addition for elements less than or equal to each other.
More concisely: For every positive number x and y > 1 in a linear ordered Archimedean semifield α, there exists an integer n such that 0 < y^n < x <= y^(n+1).
|