Set.Bounded.mono
theorem Set.Bounded.mono :
∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → Set.Bounded r t → Set.Bounded r s
The theorem `Set.Bounded.mono` states that for any type `α`, any relation `r` on `α`, and any sets `s` and `t` of type `α`, if `s` is a subset of `t` and `t` is a bounded set under the relation `r`, then `s` is also a bounded set under the relation `r`. In other words, the boundedness property of a set is preserved under taking subsets.
More concisely: If `s` is a subset of the bounded set `t` under relation `r`, then `s` is also a bounded set under relation `r`.
|
Set.bounded_gt_Ioi
theorem Set.bounded_gt_Ioi :
∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x x_1 => x > x_1) (Set.Ioi a)
This theorem states that for any type `α` with a preorder structure and for any element `a` of type `α`, the set of all elements greater than `a` (denoted by `Set.Ioi a`) is a bounded set with respect to the relation `x > x_1`. Here, a set is said to be bounded if there exists an element such that every element in the set has this relation with the specific element, and `Set.Ioi a` is the set of elements strictly greater than `a`.
More concisely: For any preorder type `α` and element `a` in `α`, the set of elements strictly greater than `a` (`Set.Ioi a`) is a bounded set with respect to the preorder relation.
|
Set.bounded_le_inter_lt
theorem Set.bounded_le_inter_lt :
∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
Set.Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Set.Bounded (fun x x_1 => x ≤ x_1) s
This theorem states that for any type `α` endowed with a linear order, a set `s` of elements of this type, and a particular element `a` of this type, the set `s` is bounded by the relation "less than or equal to" if and only if the intersection of `s` and the set of elements greater than `a` is also bounded by the same relation. In other words, a set is bounded (in the sense that every element is less than or equal to some fixed element) if its subset of elements strictly greater than a given value is also bounded in this way.
More concisely: A set of elements from a linearly ordered type is bounded if and only if its subset of elements strictly greater than a given element is also bounded.
|
Set.bounded_self
theorem Set.bounded_self : ∀ {α : Type u_1} {r : α → α → Prop} (a : α), Set.Bounded r {b | r b a}
The theorem `Set.bounded_self` states that for any type `α`, any binary relation `r` on `α`, and any element `a` of type `α`, the set of all elements `b` of type `α` such that `r b a` holds, is a bounded set. In other words, the set `{b | r b a}` is bounded, where the boundedness of a set is defined with respect to the relation `r` such that there exists an element (in this case `a` itself) for which the relation `r` holds with every element in the set.
More concisely: For any type `α` and binary relation `r` on `α`, the set `{b : α | r b a}` is bounded with respect to `r` with bound `a`.
|
Set.bounded_lt_Iio
theorem Set.bounded_lt_Iio :
∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x x_1 => x < x_1) (Set.Iio a)
The theorem `Set.bounded_lt_Iio` states that for any type `α` that has a preorder structure, and for any element `a` of `α`, the left-infinite right-open interval `(−∞, a)` is a bounded set, where the boundedness is defined with respect to the "less than" relation. In other words, there exists an element in `α` such that all elements in the interval are less than this element.
More concisely: For any type `α` with a preorder and any `a` in `α`, the left-infinite right-open interval `(−∞, a)` is a bounded set with respect to the preorder relation.
|
Set.bounded_inter_not
theorem Set.bounded_inter_not :
∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
(∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) →
∀ (a : α), Set.Bounded r (s ∩ {b | ¬r b a}) ↔ Set.Bounded r s
The theorem `Set.bounded_inter_not` states that for any type `α` and any binary relation `r` on elements of this type, and any set `s` of elements from this type, assuming a specific condition on the relation `r` holds, namely that for any two elements `a` and `b` of type `α`, there exists another element `m` such that for any element `c`, `c` being related to `a` or `b` implies `c` is also related to `m`, the boundedness of the intersection of set `s` and the set of elements not related to a given element `a` with respect to the relation `r`, is equivalent to the boundedness of set `s` itself with respect to the same relation `r`. Here, a set is considered bounded if there exists an element to which all elements of the set are related.
More concisely: For a type `α` and binary relation `r` on `α`, if for any `a` in `α`, there exists an element `m` such that any `c` related to `a` or `m` implies `c` is related to `m`, then the intersection of a set `s` with the set of elements not related to a given `a` is bounded if and only if set `s` itself is bounded with respect to `r`.
|
Set.bounded_lt_inter_not_lt
theorem Set.bounded_lt_inter_not_lt :
∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
Set.Bounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Set.Bounded (fun x x_1 => x < x_1) s
This theorem states that for any given set 's' of elements from a semilattice-supremum type 'α', and any element 'a' from the same type, the condition of 's' being a bounded set under the less-than relation is equivalent to the set formed by the intersection of 's' and the set of all elements 'b' not less than 'a' being a bounded set under the less-than relation. In mathematical terms, the property of being bounded below by a certain element in the set 's' carries over to the intersection of 's' and the elements 'b' that are not less than a given element 'a'.
More concisely: For any semilattice-supremum type 'α' and set 's' of elements from it, 's' is bounded if and only if the intersection of 's' and the set of elements greater than or equal to any given 'a' in 's' is also bounded.
|