Set.preimage_add_const_Ici
theorem Set.preimage_add_const_Ici :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => x + a) ⁻¹' Set.Ici b = Set.Ici (b - a) := by
sorry
The theorem `Set.preimage_add_const_Ici` states that for any type `α` that has an ordered additive commutative group structure, for all elements `a` and `b` of type `α`, the preimage of the set of all elements greater than or equal to `b`, under the function that adds `a` to an input, is equal to the set of all elements greater than or equal to `b - a`. In simpler terms, if you shift all the elements in a set by a constant, the preimage under this shift operation is the set where all elements are greater than or equal to the original bound minus the shift.
More concisely: For any additive commutative group `α` and elements `a, b` of `α`, the preimage of the set `{x | x ≥ b} under the function x => x + a is equal to {x | x ≥ b - a}`.
|
Set.preimage_mul_const_Iic_of_neg
theorem Set.preimage_mul_const_Iic_of_neg :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) {c : α},
c < 0 → (fun x => x * c) ⁻¹' Set.Iic a = Set.Ici (a / c)
This theorem states that for any type `α` that is a linear ordered field and any two elements `a` and `c` of this type, if `c` is less than zero, then the preimage of the set of all elements less than or equal to `a` under the function `x ↦ x * c` (i.e., the set of all `x` such that `x * c` is less than or equal to `a`) is equal to the set of all elements greater than or equal to `a / c`. In other words, multiplying by a negative constant `c` and taking the preimage reverses the direction of the inequality.
More concisely: For any linear ordered field `α` and elements `a, c` of `α` with `c < 0`, the preimage of the set of `x` with `x * c ≤ a` is equal to the set of `x` with `x ≥ a / c`.
|
Set.preimage_const_mul_Ioi
theorem Set.preimage_const_mul_Ioi :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) {c : α},
0 < c → (fun x => c * x) ⁻¹' Set.Ioi a = Set.Ioi (a / c)
This theorem states that for any type `α` that has the structure of a linearly ordered field, given any element `a` of this type and another element `c` of the same type such that `c` is greater than zero, the preimage under the function `x ↦ c * x` of the set of elements greater than `a` (i.e., the left-open right-infinite interval `(a, ∞)`) is equal to the set of elements greater than `a / c` (i.e., the left-open right-infinite interval `(a/c, ∞)`). This essentially captures the property of multiplicative scaling in ordered fields.
More concisely: For any linearly ordered field `α` and elements `a` and `c` in `α` with `c > 0`, the sets `{x : α | x > a} ` and `{x : α | x > a / c}` have equal preimages under the function `x ↦ c * x`.
|
Set.image_mul_const_uIcc
theorem Set.image_mul_const_uIcc :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a b c : α),
(fun x => x * a) '' Set.uIcc b c = Set.uIcc (b * a) (c * a)
The theorem `Set.image_mul_const_uIcc` states that for any types `α` that are linearly ordered fields and for any three instances of `α` called `a`, `b`, `c`, the image of the set `uIcc b c` under the function that multiplies each element by `a` is equal to the set `uIcc (b * a) (c * a)`. In other words, multiplying all elements in the closed interval `[b, c]` by a constant `a` results in the closed interval `[b * a, c * a]`.
More concisely: For any linearly ordered field `α` and elements `a`, `b`, `c` of `α`, the image of the interval `[b, c]` under the function that multiplies each element by `a` equals the interval `[b * a, c * a]`.
|
Set.preimage_mul_const_Iio_of_neg
theorem Set.preimage_mul_const_Iio_of_neg :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) {c : α},
c < 0 → (fun x => x * c) ⁻¹' Set.Iio a = Set.Ioi (a / c)
The theorem `Set.preimage_mul_const_Iio_of_neg` states that for any linearly ordered field `α`, given an element `a` of `α` and another element `c` of `α` which is less than zero, the preimage of the set of all elements less than `a` under multiplication with `c` is equivalent to the set of all elements greater than `a / c`. This essentially describes a transformation property of left-infinite right-open intervals under multiplication with a negative constant.
More concisely: For any linearly ordered field `α` and elements `a` and `c` of `α` with `c < 0`, the preimage of the set of elements less than `a` under multiplication by `c` is equal to the set of elements greater than `a / c`.
|
Set.preimage_neg_Iic
theorem Set.preimage_neg_Iic : ∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α), -Set.Iic a = Set.Ici (-a) := by
sorry
This theorem states that for any ordered additive commutative group (`OrderedAddCommGroup`) and any element `a` in that group, the set of all elements that are less than or equal to `a` and then negated (`-Set.Iic a`) is equal to the set of all elements that are greater than or equal to the negation of `a` (`Set.Ici (-a)`). In other words, if you negate all the elements in a right-closed left-infinite interval, you get a left-closed right-infinite interval with its bound negated.
More concisely: For any ordered additive commutative group and its element `a`, the sets `{-Set.Iic a}` and `Set.Ici (-a)` are equal.
|
Set.inv_Ioo_0_left
theorem Set.inv_Ioo_0_left :
∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α}, 0 < a → (Set.Ioo 0 a)⁻¹ = Set.Ioi a⁻¹
The theorem `Set.inv_Ioo_0_left` states that for any linearly ordered field `α` and any positive element `a` from `α`, the preimage of the interval `(0, a)` under the inverse function is the interval `(a⁻¹, ∞)`. In other words, if you take the open interval from 0 to `a` and apply the inverse function to each element in the interval, you get the open interval from `a⁻¹` to positive infinity. This theorem relates the transformation of intervals under the inverse operation in a field.
More concisely: For any linearly ordered field `α` and positive element `a` from `α`, the inverse function maps the interval `(0, a)` to the interval `(a⁻¹, ∞)`.
|
Set.preimage_const_add_Iic
theorem Set.preimage_const_add_Iic :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => a + x) ⁻¹' Set.Iic b = Set.Iic (b - a) := by
sorry
The theorem `Set.preimage_const_add_Iic` states that for any ordered additive commutative group `α` and any elements `a` and `b` of `α`, the preimage of the left-infinite right-closed interval ending at `b` under the function that adds `a` to its input is the left-infinite right-closed interval ending at `b - a`. In other words, shifting all points in the interval down by `a` has the effect of moving the endpoint of the interval from `b` to `b - a`.
More concisely: For any ordered additive commutative group (α, +) and elements a, b of α, the preimage of the left-infinite right-closed interval Ic[b] under the function x ↦ x + a is equal to Ic[b - a].
|
Set.preimage_mul_const_Ioi_of_neg
theorem Set.preimage_mul_const_Ioi_of_neg :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) {c : α},
c < 0 → (fun x => x * c) ⁻¹' Set.Ioi a = Set.Iio (a / c)
This theorem states that for any linearly ordered field `α` and any elements `a` and `c` of `α` such that `c` is less than 0, the preimage of the function `x * c` on the set `Set.Ioi a` (which denotes an interval `(a, +∞)`) is equal to the set `Set.Iio (a / c)` (which denotes an interval `(-∞, a / c)`). In other words, if you multiply each element `x` in the field by `c` and consider the resulting set of elements greater than `a`, it is equivalent to considering all the elements less than `a / c` in the original field.
More concisely: For any linearly ordered field `α` and elements `a, c ∈ α` with `c < 0`, the sets `{x ∈ α | x > a} ` and `{x ∈ α | x < a / c}` are equal.
|
Set.abs_sub_right_of_mem_uIcc
theorem Set.abs_sub_right_of_mem_uIcc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c : α}, c ∈ Set.uIcc a b → |b - c| ≤ |b - a|
The theorem `Set.abs_sub_right_of_mem_uIcc` states that, given a linearly ordered additive commutative group `α` and the elements `a`, `b`, and `c` of this group, if `c` is in the set `uIcc a b` (which represents all the elements lying between `a` and `b`, including `a` and `b`), then the absolute value of the difference between `b` and `c` is less than or equal to the absolute value of the difference between `b` and `a`. In other words, the distance between `c` and `b` is not greater than the distance between `a` and `b` when `c` is within the interval `[a, b]`.
More concisely: For all linearly ordered additive commutative groups α and elements a, b, and c, if c ∈ uIcc a b then |b - a| ≥ |b - c|.
|
Set.preimage_add_const_Iic
theorem Set.preimage_add_const_Iic :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => x + a) ⁻¹' Set.Iic b = Set.Iic (b - a) := by
sorry
The theorem `Set.preimage_add_const_Iic` states that for any ordered additive commutative group `α`, and any elements `a` and `b` of `α`, the preimage of the set of elements less than or equal to `b` under the function that adds `a` to its input is the set of elements less than or equal to `b - a`. In other words, if we take a set of all elements that are less than or equal to `b`, and then apply the function that adds `a` to each element, the set we get is exactly the set of all elements that are less than or equal to `b - a`.
More concisely: For any ordered additive commutative group (α, +) and elements a, b ∈ α, the preimage of the set {x ∈ α : x ≤ b} under the function x => x + a is the set {x ∈ α : x ≤ b - a}.
|
Set.abs_sub_left_of_mem_uIcc
theorem Set.abs_sub_left_of_mem_uIcc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c : α}, c ∈ Set.uIcc a b → |c - a| ≤ |b - a|
This theorem states that for any Linearly Ordered Additive Commutative Group, given elements 'a', 'b', and 'c', if 'c' belongs to the set of elements between 'a' and 'b' (inclusive), then the absolute difference between 'c' and 'a' is less than or equal to the absolute difference between 'b' and 'a'. In other words, the distance from 'a' to 'c' is never greater than the distance from 'a' to 'b' when 'c' lies in the interval from 'a' to 'b'.
More concisely: For any Linearly Ordered Additive Commutative Group, if element 'c' lies between 'a' and 'b' (inclusive), then |a - c| <= |b - a|.
|
Set.preimage_neg_Ici
theorem Set.preimage_neg_Ici : ∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α), -Set.Ici a = Set.Iic (-a) := by
sorry
This theorem states that for any ordered additive commutative group `α` and any element `a` in `α`, the set of all elements `x` such that `-a` is less than or equal to `x` (`-Set.Ici a`), is equal to the set of all elements `x` such that `x` is less than or equal to `-a` (`Set.Iic (-a)`). In other words, negating the set of all elements greater than or equal to a certain value yields the set of all elements less than or equal to the negation of that value.
More concisely: For any ordered additive commutative group `α` and its element `a`, the sets `-Set.Ici a` and `Set.Iic (-a)` are equal.
|
Set.preimage_add_const_Iio
theorem Set.preimage_add_const_Iio :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => x + a) ⁻¹' Set.Iio b = Set.Iio (b - a) := by
sorry
This theorem, `Set.preimage_add_const_Iio`, asserts that for any ordered additive commutative group `α`, and for any two elements `a` and `b` of `α`, the preimage of the set of elements less than `b` under the function that adds `a` to each element is the set of elements less than `b - a`. In other words, if we shift all elements in the group by `a`, those that were less than `b` before the shift are now less than `b - a`.
More concisely: For any ordered additive commutative group `α` and elements `a, b` in `α`, the preimage of the set of elements less than `b` under the function `x => x + a` is the set of elements less than `b - a`.
|
Set.preimage_neg_Ioo
theorem Set.preimage_neg_Ioo :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), -Set.Ioo a b = Set.Ioo (-b) (-a)
The theorem `Set.preimage_neg_Ioo` states that for any ordered additive commutative group `α`, and any two elements `a` and `b` of `α`, the negation of the interval `(a, b)` (that is, all elements `x` in the group such that `a < x < b`) is equal to the interval `(-b, -a)`. In other words, if you take all the elements between `a` and `b` and negate them, you get all the elements between `-b` and `-a`.
More concisely: For any ordered additive commutative group `α` and elements `a` and `b` in `α`, the negation of the interval `(a, b)` equals the interval `(-b, -a)`.
|
Set.preimage_neg_Icc
theorem Set.preimage_neg_Icc :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), -Set.Icc a b = Set.Icc (-b) (-a)
The theorem `Set.preimage_neg_Icc` states that for any ordered additive commutative group `α` and any two elements `a` and `b` from `α`, the negation of the closed interval from `a` to `b` is equal to the closed interval from `-b` to `-a`. In simpler terms, if you have a closed interval between two numbers, flipping this interval around zero (negating all the values in the interval) results in a new closed interval that runs from the negation of the original upper bound to the negation of the original lower bound.
More concisely: For any ordered additive commutative group α and elements a, b ∈ α, the negation of the closed interval Icc (a, b) equals Icc (-b, -a).
|
Set.preimage_mul_const_Ici_of_neg
theorem Set.preimage_mul_const_Ici_of_neg :
∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) {c : α},
c < 0 → (fun x => x * c) ⁻¹' Set.Ici a = Set.Iic (a / c)
The theorem `Set.preimage_mul_const_Ici_of_neg` states that for any type `α` which is a linear ordered field, a value `a` of type `α`, and a value `c` of type `α` that is less than zero, the preimage of the set of all `x` such that `a` is less than or equal to `x * c` is equal to the set of all `x` such that `x` is less than or equal to `a / c`. In mathematical terms, for a negative constant `c`, the operation of multiplying by `c` transforms the interval `[a, ∞)` to `(-∞, a/c]`.
More concisely: For any linear ordered field `α`, `a : α` with `c : α` negative, the set inverse images under multiplication by `c` of the sets `{x : α | a ≤ x}` and `{x : α | x ≤ a / c}` are equal.
|
Set.preimage_neg_Ioi
theorem Set.preimage_neg_Ioi : ∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α), -Set.Ioi a = Set.Iio (-a) := by
sorry
This theorem, `Set.preimage_neg_Ioi`, states that for any type `α` that has an ordered additive commutative group structure, for any element `a` of `α`, the negation of the set of all elements greater than `a` (`-Set.Ioi a`) is equal to the set of all elements less than `-a` (`Set.Iio (-a)`). In other words, if you take all the numbers greater than a certain value, negate them, you end up with all of the numbers less than the negation of that value.
More concisely: For any ordered additive commutative group `α` and element `a` in `α`, `-Set.Ioi a = Set.Iio (-a)`. In other words, the negative of the set of elements strictly greater than `a` is equal to the set of elements strictly less than `-a`.
|
Set.preimage_const_add_Ici
theorem Set.preimage_const_add_Ici :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => a + x) ⁻¹' Set.Ici b = Set.Ici (b - a) := by
sorry
This theorem states that for any ordered additive commutative group `α` and any elements `a` and `b` of `α`, the preimage of the set of all elements `x` in `α` such that `b` is less than or equal to `a + x` under the function that maps `x` to `a + x` is the set of all elements `x` in `α` such that `b - a` is less than or equal to `x`. In more mathematical terms, for any `a` and `b` in some ordered additive commutative group, the preimage of the interval `[b, ∞)` under the function `f(x) = a + x` is the interval `[b - a, ∞)`.
More concisely: For any ordered additive commutative group `α` and elements `a, b` in `α`, the preimage of the interval `[b, ∞)` under the function `x mapsto a + x` is the interval `[b - a, ∞)`.
|
Set.preimage_const_add_Ioi
theorem Set.preimage_const_add_Ioi :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => a + x) ⁻¹' Set.Ioi b = Set.Ioi (b - a) := by
sorry
The theorem `Set.preimage_const_add_Ioi` states that for any ordered additive commutative group `α` and any elements `a` and `b` in `α`, the preimage of the set of all elements greater than `b` under the function `x => a + x` is equal to the set of all elements greater than `b - a`. In simpler terms, if you add a constant `a` to every element in the group and then take all the elements greater than `b`, it's the same as if you just took all the group elements greater than `b - a` to begin with.
More concisely: For any ordered additive commutative group `α` and elements `a, b` in `α`, `(a +)⁻¹'{x : α | x > b} = {x : α | x > b - a}`.
|
Set.preimage_add_const_Ioi
theorem Set.preimage_add_const_Ioi :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => x + a) ⁻¹' Set.Ioi b = Set.Ioi (b - a) := by
sorry
The theorem `Set.preimage_add_const_Ioi` states that for any ordered additive commutative group `α` and any elements `a` and `b` from `α`, the preimage of the set of elements greater than `b` under the function `x ↦ x + a` is equal to the set of elements greater than `b - a`. In other words, if you shift all elements in the group by `a`, the set of elements that were greater than `b` before the shift is the same as the set of elements that are greater than `b - a` after the shift.
More concisely: For any ordered additive commutative group α and elements a, b from α, the preimage of the set {x : α | x > b} under the function x ↦ x + a is equal to {x : α | x > b - a}.
|
Set.abs_sub_le_of_uIcc_subset_uIcc
theorem Set.abs_sub_le_of_uIcc_subset_uIcc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c d : α},
Set.uIcc c d ⊆ Set.uIcc a b → |d - c| ≤ |b - a|
The theorem `Set.abs_sub_le_of_uIcc_subset_uIcc` states that for any subtype α, which is a linear ordered additive commutative group, and any elements a, b, c, d of this type, if the interval [c, d] is a subset of the interval [a, b] (represented by the condition '`Set.uIcc c d ⊆ Set.uIcc a b`'), then the absolute difference between c and d is less than or equal to the absolute difference between a and b, denoted as '|d - c| ≤ |b - a|'. This theorem basically asserts that if one interval is contained within another, then the length or "distance" of the inner interval is not larger than the length or "distance" of the outer interval.
More concisely: If $c, d, a, b$ are elements of a linear ordered additive commutative group $\alpha$, then $|d-c|\leq|b-a|$ whenever $[c,d]\subseteq[a,b]$.
|
Set.preimage_add_const_uIcc
theorem Set.preimage_add_const_uIcc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a b c : α),
(fun x => x + a) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
The theorem `Set.preimage_add_const_uIcc` states that for any linearly ordered additive commutative group `α` and any elements `a`, `b`, and `c` of `α`, the preimage of the set of elements lying between `b` and `c` (inclusive) under the function that adds `a` to each element is the set of elements lying between `b - a` and `c - a` (inclusive). In other words, shifting all elements in a set by a constant `a` in this group corresponds to shifting the lower and upper bounds of the set by `-a`.
More concisely: For any linearly ordered additive commutative group α and elements a, b, and c of α, the preimage of the set {x : α | b ≤ x ≤ c} under the function x => x + a is {x : α | b - a ≤ x ≤ c - a}.
|
Set.preimage_neg_Iio
theorem Set.preimage_neg_Iio : ∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α), -Set.Iio a = Set.Ioi (-a) := by
sorry
This theorem states that for any type `α` that forms an Ordered Additive Commutative Group, the preimage of the left-infinite, right-open interval under negation, `-Set.Iio a`, is equal to the left-open right-infinite interval at `-a`, `Set.Ioi (-a)`. In other words, if you take all elements less than a certain value `a` in this ordered group, negate them, you will get a set of all elements greater than `-a`.
More concisely: For any Ordered Additive Commutative Group `α`, the set of all elements negated from elements in the left-open right-infinite interval `Set.Ioi (-a)` is equal to the preimage of the left-infinite, right-open interval `-Set.Iio a` under negation.
|
Set.preimage_const_add_Iio
theorem Set.preimage_const_add_Iio :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α), (fun x => a + x) ⁻¹' Set.Iio b = Set.Iio (b - a) := by
sorry
This theorem states that for any ordered additive commutative group `α`, and any two elements 'a' and 'b' of this group, the preimage of the set of elements less than 'b' under the function that adds 'a' to each element is the set of elements less than 'b - a'. In other words, if we shift each element of 'α' by 'a' to the right, the elements that were less than 'b' before the shift are precisely those that are less than 'b - a' after the shift.
More concisely: For any ordered additive commutative group `α` and elements `a, b` of `α`, the set `{x : α | x < b}` is equal to the set `{x : α | x + a < b}`.
|