IsUpperSet.smul
theorem IsUpperSet.smul :
∀ {α : Type u_1} [inst : OrderedCommGroup α] {s : Set α} {a : α}, IsUpperSet s → IsUpperSet (a • s)
The theorem `IsUpperSet.smul` states that for any ordered commutative group `α`, any set `s` of elements of this group, and any element `a` of the group, if `s` is an upper set (meaning that for any elements `a` and `b` in `α`, if `a` is less than or equal to `b` and `a` is in `s`, then `b` is also in `s`), then the set obtained by multiplying every element of `s` by `a` (denoted as `a • s`) is also an upper set.
More concisely: If `s` is an upper set in an ordered commutative group `α`, then the set `a • s` obtained by multiplying every element of `s` by an element `a` in `α` is also an upper set.
|
IsUpperSet.mul_left
theorem IsUpperSet.mul_left :
∀ {α : Type u_1} [inst : OrderedCommGroup α] {s t : Set α}, IsUpperSet t → IsUpperSet (s * t)
The theorem `IsUpperSet.mul_left` states that for any ordered commutative group `α` and any two sets `s` and `t` within `α`, if `t` is an upper set, then the product of `s` and `t` (denoted as `s * t`) is also an upper set. An upper set, in this context, is a set such that if any element `b` is greater than an element `a` in the set, then `b` is also in the set. In other words, once an element is in an upper set, all elements greater than it are also in the set. So, the theorem is about the preservation of the upper set property under multiplication with any other set in an ordered commutative group.
More concisely: If `α` is an ordered commutative group and `t` is an upper set in `α`, then the product `s * t` is an upper set for any set `s` in `α`.
|
add_lowerClosure
theorem add_lowerClosure :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (s t : Set α), s + ↑(lowerClosure t) = ↑(lowerClosure (s + t)) := by
sorry
This theorem, `add_lowerClosure`, states that for any type `α` that forms an ordered additive commutative group, given any two sets `s` and `t` of this type, the sum of the set `s` and the lower closure of `t` is equal to the lower closure of the sum of `s` and `t`. In mathematical terms, this theorem demonstrates the distributive property of the lower closure over the operation of addition of sets in such a group.
More concisely: For any ordered additive commutative group type `α`, the lower closure of `s + t` equals the lower closure of `s` + lower closure of `t`.
|
IsUpperSet.mul_right
theorem IsUpperSet.mul_right :
∀ {α : Type u_1} [inst : OrderedCommGroup α] {s t : Set α}, IsUpperSet s → IsUpperSet (s * t)
The theorem `IsUpperSet.mul_right` states that for any ordered commutative group `α` and any two sets `s` and `t` of elements of `α`, if `s` is an upper set (i.e., a set where any element greater than one of its members is also a member), then the product set `s * t` (formed by multiplying elements from `s` and `t`) is also an upper set.
More concisely: If `s` is an upper set in a commutative group `α`, then the product set `s * t` is also an upper set for any set `t` in `α`.
|
IsUpperSet.add_left
theorem IsUpperSet.add_left :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] {s t : Set α}, IsUpperSet t → IsUpperSet (s + t)
The theorem `IsUpperSet.add_left` states that for every type `α` which forms an ordered additive commutative group, if `t` is an upper set, then the set formed by adding every element of another set `s` to every element of `t` is also an upper set. In other words, if `t` is an upper set, the upward-closure property is maintained under the operation of left-addition by elements from the set `s`.
More concisely: If `t` is an upper set in an ordered additive commutative group `α`, then the set `{x + y | x ∈ t, y ∈ s}` is also an upper set.
|
mul_upperClosure
theorem mul_upperClosure :
∀ {α : Type u_1} [inst : OrderedCommGroup α] (s t : Set α), s * ↑(upperClosure t) = ↑(upperClosure (s * t)) := by
sorry
This theorem states that for any ordered commutative group `α` and any two sets `s` and `t` of elements in `α`, the set resulting from multiplying every element of `s` by the upper closure of `t` (i.e., the smallest subset of `α` that contains `t` and is closed under taking an element greater than or equal to any given one) is equal to the upper closure of the set resulting from multiplying every element of `s` by every element of `t`. In mathematical terms, we have $s \cdot \overline{t} = \overline{s \cdot t}$ where $\overline{T}$ denotes the upper closure of a set $T$.
More concisely: For any ordered commutative group `α` and sets `s` and `t` in `α`, the upper closures of `s * t` and `s * Cl(t)` are equal, where `*` denotes multiplication and `Cl(t)` is the upper closure of `t`.
|
IsUpperSet.vadd
theorem IsUpperSet.vadd :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] {s : Set α} {a : α}, IsUpperSet s → IsUpperSet (a +ᵥ s)
The theorem `IsUpperSet.vadd` states that for any type `α` that forms an ordered additive commutative group and any set `s` of this type, along with any element `a` of this type, if `s` is an upper set (meaning that if any element `b` is greater than or equal to any element in `s`, then `b` is also in `s`), then the set obtained by adding `a` to every element in `s` (denoted as `a +ᵥ s`) is also an upper set.
More concisely: If `α` is an ordered additive commutative group, `s` is an upper set of `α`, then `a +ᵥ s` is also an upper set of `α` for any `a` in `α`.
|
add_upperClosure
theorem add_upperClosure :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (s t : Set α), s + ↑(upperClosure t) = ↑(upperClosure (s + t)) := by
sorry
This theorem states that for any ordered additive commutative group `α` and any sets `s` and `t` of elements of `α`, the set obtained by adding every element of `s` to every element of the upper closure of `t` (the set of all elements greater than or equal to some element in `t`) is equal to the upper closure of the set obtained by adding every element of `s` to every element of `t`. In other words, the process of adding a set to the upper closure of another set is the same as first adding the two sets and then taking the upper closure.
More concisely: For any ordered additive commutative group `α` and sets `s` and `t`, the upper closure of `s` + upper closure(`t`) equals the upper closure of `s` + `t`.
|
IsUpperSet.add_right
theorem IsUpperSet.add_right :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] {s t : Set α}, IsUpperSet s → IsUpperSet (s + t)
This theorem states that for any ordered additive commutative group `α` and any two sets `s` and `t` of `α`, if `s` is an upper set (that is, every element of `s` is less than or equal to every other element of `s`), then the set `s + t` (which consists of the sums of all possible pairs of elements, one from `s` and the other from `t`) is also an upper set.
More concisely: If `s` is an upper set in an ordered additive commutative group `α`, then `s + t` is an upper set for any set `t` in `α`.
|
mul_lowerClosure
theorem mul_lowerClosure :
∀ {α : Type u_1} [inst : OrderedCommGroup α] (s t : Set α), s * ↑(lowerClosure t) = ↑(lowerClosure (s * t)) := by
sorry
This theorem states that for any ordered commutative group `α` and any two sets `s` and `t` of elements from `α`, the product of `s` and the least lower set containing `t` is equal to the least lower set containing the product of `s` and `t`. In mathematical terms, given two sets `s` and `t` in an ordered commutative group, `s * lowerClosure(t) = lowerClosure(s * t)`. Here, the `lowerClosure` of a set is the set of all elements that are less than or equal to some element in the given set; and the multiplication `*` is done element-by-element.
More concisely: For any ordered commutative group `α` and sets `s` and `t` in `α`, the least lower sets of `s * t` and `s` intersecting `t` are equal. (Equivalently, `s * lowerClosure(t) = lowerClosure(s * t)`.)
|