LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self
theorem LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedField α] [inst_1 : ConditionallyCompleteLinearOrderedField β]
[inst_2 : Archimedean α] {a : α},
0 < a →
∀ b < LinearOrderedField.inducedMap α β a * LinearOrderedField.inducedMap α β a,
∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c
This theorem, named `LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`, is a preparatory lemma for `inducedOrderRingHom`. It states that for all linear ordered fields `α` and conditionally complete linear ordered fields `β` with archimedean property, given an element `a` in `α` that is greater than zero, if there exists another element `b` that is less than the square of the image of `a` under the induced order preserving function from `α` to `β`, then there exists an element `c` in the 'cut' set (set of all rationals less than `a*a` taken in the field `β`) such that `b` is less than `c`. The 'cut' set is formed by projecting the set of elements of `α` less than `a*a` under the function that casts rationals to `β`.
More concisely: For all linear ordered fields `α` and conditionally complete linear ordered fields `β` with archimedean property, if `a` is a positive element in `α` and there exists `b` in `β` such that `b < a^2 * (image of a under induced function)`, then there exists `c` in the 'cut' set of `β` such that `b < c`.
|
ConditionallyCompleteLinearOrderedField.le_csInf
theorem ConditionallyCompleteLinearOrderedField.le_csInf :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α) (a : α),
s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
This theorem states that for any set `s` of a type `α` that forms a conditionally complete linearly ordered field, and for any element `a` of `α`, if the set `s` is nonempty and the element `a` belongs to the lower bounds of `s`, then `a` is less than or equal to the infimum (`sInf`) of `s`. In other words, all elements in the set of lower bounds of `s` are less than or equal to the infimum of `s`.
More concisely: For any conditionally complete linearly ordered field `s` of type `α` with nonempty lower bounds, every element `a` in the lower bounds satisfies `a ≤ s.inf`.
|
LinearOrderedField.cutMap_nonempty
theorem LinearOrderedField.cutMap_nonempty :
∀ {α : Type u_2} (β : Type u_3) [inst : LinearOrderedField α] [inst_1 : LinearOrderedField β]
[inst_2 : Archimedean α] (a : α), (LinearOrderedField.cutMap β a).Nonempty
The theorem `LinearOrderedField.cutMap_nonempty` asserts that for any given type `α` with a linear ordered field structure, another type `β` with a linear ordered field structure as well, and an element `a` of type `α` under the assumption that `α` is Archimedean, the set of elements of type `β` that are less than `a` (obtained via the `cutMap` function) is nonempty. In other words, there is always at least one element of type `β` that is less than any given element of type `α` in an Archimedean linearly ordered field.
More concisely: In an Archimedean linearly ordered field, the set of elements of another linearly ordered field that are strictly less than any given element is nonempty.
|
LinearOrderedField.coe_lt_inducedMap_iff
theorem LinearOrderedField.coe_lt_inducedMap_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedField α] [inst_1 : ConditionallyCompleteLinearOrderedField β]
[inst_2 : Archimedean α] {a : α} {q : ℚ}, ↑q < LinearOrderedField.inducedMap α β a ↔ ↑q < a
This theorem states that for all types `α` and `β`, where `α` is a linear ordered field and `β` is a conditionally complete linear ordered field, and where `α` is also Archimedean, for any element `a` of type `α` and any rational number `q`, the condition that the rational `q` is less than the image of `a` under the induced order preserving function from `α` to `β` is equivalent to `q` being less than `a`. In mathematical terms, the theorem asserts that for an arbitrary real number `a` and rational `q`, the inequality $q < \sup\{r \in \mathbb{Q} : r < a\}$ holds if and only if $q < a$.
More concisely: For any Archimedean linear ordered field `α` and conditionally complete linear ordered field `β`, the image of an element `a` from `α` under the order-preserving function to `β` is equal to the supreme element in the set of rationals strictly less than `a`. That is, for all `a` in `α` and rational `q`, `q < a` if and only if `q < sup {r : ℚ | r < a}`.
|
LinearOrderedField.cutMap_bddAbove
theorem LinearOrderedField.cutMap_bddAbove :
∀ {α : Type u_2} (β : Type u_3) [inst : LinearOrderedField α] [inst_1 : LinearOrderedField β]
[inst_2 : Archimedean α] (a : α), BddAbove (LinearOrderedField.cutMap β a)
This theorem states that for all types `α` and `β`, if `α` is a linearly ordered field, `β` is also a linearly ordered field, and `α` is Archimedean, then for any element `a` of type `α`, the set of all elements of type `β` that are less than `a` (as defined by the `LinearOrderedField.cutMap` function) is bounded above. In other words, there exists an upper bound for this set. This is true for any linearly ordered field that satisfies the Archimedean property, such as the real numbers.
More concisely: For any linearly ordered fields `α` and `β` with `α` Archimedean, the set of elements in `β` less than an arbitrary element in `α` is bounded above.
|
LinearOrderedField.inducedMap_rat
theorem LinearOrderedField.inducedMap_rat :
∀ (α : Type u_2) (β : Type u_3) [inst : LinearOrderedField α] [inst_1 : ConditionallyCompleteLinearOrderedField β]
[inst_2 : Archimedean α] (q : ℚ), LinearOrderedField.inducedMap α β ↑q = ↑q
The theorem `LinearOrderedField.inducedMap_rat` states that for all types `α` and `β` where `α` is a linear ordered field, `β` is a conditionally complete linear ordered field, and `α` is Archimedean, the result of applying the induced map function from the linear ordered field to the conditionally complete linear ordered field on a rational number `q` is the same as the original rational number `q`. More formally, for every rational number `q`, the supremum in `β` of all the elements of `α` less than `q` is equivalent to `q`.
More concisely: For every Archimedean linear ordered field `α` and conditionally complete linear ordered field `β`, the induced map from `α` to `β` maps every rational number `q` to the supremum of all elements in `α` less than `q`.
|
ConditionallyCompleteLinearOrderedField.inf_le_right
theorem ConditionallyCompleteLinearOrderedField.inf_le_right :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b : α), a ⊓ b ≤ b
This theorem states that for any type `α` that has the structure of a conditionally complete linear ordered field, the infimum (`inf` or `⊓`) of two elements `a` and `b` of type `α` is less than or equal to `b`. In other words, if you take any two elements from a conditionally complete linear ordered field and calculate their infimum, the result will always be a lower bound of the second element.
More concisely: For any conditionally complete linear ordered field `α`, the infimum of `a` and `b` in `α` satisfies `inf a b ≤ b`.
|
ConditionallyCompleteLinearOrderedField.inf_le_left
theorem ConditionallyCompleteLinearOrderedField.inf_le_left :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b : α), a ⊓ b ≤ a
This theorem states that for any type `α` that has a property of a `ConditionallyCompleteLinearOrderedField`, the infimum ("greatest lower bound") of any two elements `a` and `b` of type `α` is less than or equal to `a`. In simpler terms, it states that the infimum of two elements in such a field is always a lower bound for each of the elements.
More concisely: For any Conditionally Complete Linearly Ordered Field `α`, the infinfum of elements `a` and `b` in `α` satisfies `inf(a, b) ≤ a`.
|
ConditionallyCompleteLinearOrderedField.le_inf
theorem ConditionallyCompleteLinearOrderedField.le_inf :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c := by
sorry
This theorem states that for any conditionally complete linearly ordered field, for any three elements `a`, `b`, `c` of this field, if `a` is less than or equal to `b` and `a` is less than or equal to `c`, then `a` is less than or equal to the infimum of `b` and `c` (symbolized by `b ⊓ c`). In other words, the infimum of `b` and `c` is the greatest lower bound for the set of all elements that are less than or equal to both `b` and `c`.
More concisely: In a conditionally complete linearly ordered field, for all elements `a`, `b`, `c`, if `a` is less than or equal to both `b` and `c`, then `a` is less than or equal to the infimum of `b` and `c` (`b ⊓ c`).
|
ConditionallyCompleteLinearOrderedField.le_csSup
theorem ConditionallyCompleteLinearOrderedField.le_csSup :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α) (a : α),
BddAbove s → a ∈ s → a ≤ sSup s
This theorem asserts that in a conditionally complete linearly ordered field, for any given set `s` and any element `a` in `s`, if `s` is bounded above (`BddAbove s`), then `a` is less than or equal to the supremum of `s` (`sSup s`). In other words, every element of a bounded above set is less than or equal to the supremum of that set in the context of a conditionally complete linearly ordered field. The conditionally complete linearly ordered field is a mathematical structure that has properties of both ordered fields (like the real numbers) and conditionally complete lattices.
More concisely: In a conditionally complete linearly ordered field, every bounded above element is less than or equal to the supremum.
|
ConditionallyCompleteLinearOrderedField.csInf_le
theorem ConditionallyCompleteLinearOrderedField.csInf_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α) (a : α),
BddBelow s → a ∈ s → sInf s ≤ a
This theorem states that for any set `s` of a particular type `α`, where `α` is a conditionally complete linearly ordered field, if `s` is bounded below ("BddBelow s"), and an element `a` belongs to this set (`a ∈ s`), then the infimum (greatest lower bound) of the set `s` (`sInf s`) is less than or equal to the element `a`. In other words, every element of the set is greater than or equal to the greatest lower bound of the set.
More concisely: For any set `s` of a conditionally complete linearly ordered field `α` that is bounded below and contains an element `a`, the infimum of `s` is less than or equal to `a`. (i.e. `sInf s ≤ a`)
|
LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap
theorem LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrderedField α] [inst_1 : ConditionallyCompleteLinearOrderedField β]
[inst_2 : Archimedean α] {a : α},
0 < a →
∀ b ∈ LinearOrderedField.cutMap β (a * a),
b ≤ LinearOrderedField.inducedMap α β a * LinearOrderedField.inducedMap α β a
This theorem, named `LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap`, states that for any two types `α` and `β`, where `α` is a linear ordered field and `β` is a conditionally complete linear ordered field, and `α` is also Archimedean, if `a` is an element of `α` and is positive, then, for every `b` in the lower cut of rationals in `β` that are less than `a * a`, `b` is less than or equal to the square of the supremum in `β` of all the rationals less than `a`.
To put it more simply, it says that for a positive element `a` in an Archimedean field, the square of the supremum of all rationals less than `a` in the associated complete field is an upper bound for the set of all elements less than `a * a`.
More concisely: For any Archimedean linear ordered field `α` and conditionally complete linear ordered field `β`, if `a` is a positive element of `α`, then the square of the supremum of rationals in `β` less than `a` is an upper bound for those rationals in `β` that are less than `a * a`.
|
ConditionallyCompleteLinearOrderedField.csInf_of_not_bddBelow
theorem ConditionallyCompleteLinearOrderedField.csInf_of_not_bddBelow :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α), ¬BddBelow s → sInf s = sInf ∅ := by
sorry
This theorem states that for any type `α` which has the structure of a Conditionally Complete Linear Ordered Field, if a set `s` of this type is not bounded below (meaning there doesn't exist a lower bound for the elements in the set), then the greatest lower bound (infimum) of this set `s` is by default equal to the greatest lower bound (infimum) of the empty set.
More concisely: If `α` is a Conditionally Complete Linear Ordered Field and `s ⊆ α` has no lower bound, then the infimum of `s` equals the infimum of the empty set.
|
ConditionallyCompleteLinearOrderedField.csSup_le
theorem ConditionallyCompleteLinearOrderedField.csSup_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α) (a : α),
s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
This theorem states that for any set `s` of a type `α`, where `α` is a conditionally complete linearly ordered field, and for any element `a` of type `α`, if `s` is a nonempty set and `a` is an upper bound of `s`, then the supremum of `s` (denoted as `sSup s`) is less than or equal to `a`.
In other words, if `s` is a nonempty set and `a` belongs to the set of upper bounds of `s`, then the least upper bound (or supremum) of `s` is not greater than `a`. This is a reflection of the property of supremum in ordered fields, which states that the supremum of a set is the smallest upper bound that the set can have.
More concisely: If `α` is a conditionally complete linearly ordered field and `s` is a nonempty subset of `α` with upper bound `a`, then `sSup s ≤ a`.
|
ConditionallyCompleteLinearOrderedField.le_sup_right
theorem ConditionallyCompleteLinearOrderedField.le_sup_right :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b : α), b ≤ a ⊔ b
This theorem states that for any conditionally complete linearly ordered field (like the real numbers), the supremum (`⊔`, also commonly known as the "least upper bound" or "join") of any two elements `a` and `b` in this field is an upper bound for `b`. In other words, `b` is less than or equal to `a ⊔ b` for all `a`, `b` in this field.
More concisely: For any conditionally complete linearly ordered field, the supremum of two elements is an upper bound for the second element.
|
ConditionallyCompleteLinearOrderedField.sup_le
theorem ConditionallyCompleteLinearOrderedField.sup_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c := by
sorry
This theorem states that in a conditionally complete linearly ordered field, the supremum (or least upper bound) of two elements `a` and `b` is less than or equal to a third element `c` if both `a` and `b` are less than or equal to `c`. Specifically, for any type `α` that has the structure of a conditionally complete linearly ordered field, and any three elements `a`, `b`, and `c` of type `α`, if `a` and `b` are each less than or equal to `c`, then the supremum of `a` and `b` is also less than or equal to `c`.
More concisely: In a conditionally complete linearly ordered field, the supremum of two elements is less than or equal to a third element if both elements are less than or equal to that third element.
|
ConditionallyCompleteLinearOrderedField.le_sup_left
theorem ConditionallyCompleteLinearOrderedField.le_sup_left :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (a b : α), a ≤ a ⊔ b
This theorem states that for any conditionally complete linearly ordered field, the supremum (or least upper bound) of any two elements from this field is an upper bound on the first of these two elements. In other words, for any type `α` that forms such a field, and for any two elements `a` and `b` of this type, `a` is less than or equal to the supremum of `a` and `b`.
More concisely: For any conditionally complete linearly ordered field, the supremum of any two elements is an upper bound for the first element.
|
ConditionallyCompleteLinearOrderedField.csSup_of_not_bddAbove
theorem ConditionallyCompleteLinearOrderedField.csSup_of_not_bddAbove :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderedField α] (s : Set α), ¬BddAbove s → sSup s = sSup ∅ := by
sorry
This theorem states that if a set, within the context of a conditionally complete linearly ordered field, is not bounded above, then its supremum (the least upper bound) is, by convention, the supremum of the empty set. In other words, for any set 's' in a conditionally complete linearly ordered field, if 's' does not have an upper bound, then the least upper bound of 's' is equal to the least upper bound of the empty set.
More concisely: In a conditionally complete linearly ordered field, if a set has no upper bound, then its supremum equals the supremum of the empty set.
|