LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Order.Bounds.Basic

`IsLUB.bddAbove` theorem IsLUB.bddAbove : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → BddAbove s The theorem `IsLUB.bddAbove` states that for any type `α` with a preorder structure, for any set `s` of elements of this type, and for any element `a` of this type, if `a` is a least upper bound of the set `s`, then the set `s` is bounded from above. In other words, if there exists an element that is the smallest element greater than or equal to every element in the set, then there exists an element that is greater than or equal to every element in the set. More concisely: For any preordered type `α` and set `s` of elements in `α`, if `a` is the least upper bound of `s`, then `s` is bounded above by `a`.
`Monotone.map_bddAbove` theorem Monotone.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, BddAbove s → BddAbove (f '' s) This theorem states that if a set, say 's', within a preordered type, 'α', is bounded above, then the image of this set under a monotone function, 'f', from 'α' to another preordered type, 'β', is also bounded above. In simpler terms, a monotone function won't be able to "break" an upper bound of a set, meaning if the original set is bounded above, its image after the function is applied will be bounded above as well. More concisely: If `s` is a bounded above subset of a preordered type `α` and `f` is a monotone function from `α` to a preordered type `β`, then the image `f''s` is also a bounded above subset of `β`.
`isLUB_pair` theorem isLUB_pair : ∀ {γ : Type w} [inst : SemilatticeSup γ] {a b : γ}, IsLUB {a, b} (a ⊔ b) The theorem `isLUB_pair` states that for any given type `γ` equipped with a semilattice structure, and any two elements `a` and `b` of this type, the join of `a` and `b` (denoted by `a ⊔ b`) is a least upper bound of the set containing `a` and `b`. In other words, the join of `a` and `b` is the smallest element that is greater than or equal to both `a` and `b`. This is a property characteristic of semilattices. More concisely: For any semilattice type `γ` and elements `a` and `b` in `γ`, `a ⊔ b` is the least element that is greater than or equal to both `a` and `b`.
`IsLUB.of_subset_of_superset` theorem IsLUB.of_subset_of_superset : ∀ {α : Type u} [inst : Preorder α] {a : α} {s t p : Set α}, IsLUB s a → IsLUB p a → s ⊆ t → t ⊆ p → IsLUB t a := by sorry The theorem `IsLUB.of_subset_of_superset` states that, in the context of a preorder, if a certain element `a` is a least upper bound (LUB) for two sets `s` and `p`, then `a` is also a LUB for any other set `t` that is a superset of `s` and a subset of `p`. In other words, if `s ⊆ t ⊆ p`, and `a` is a LUB for both `s` and `p`, then `a` will also be a LUB for `t`. More concisely: If `a` is the least upper bound of sets `s` and `p` in a preorder, then `a` is also the least upper bound of any set `t` that is a superset of `s` and a subset of `p`.
`BddBelow.inter_of_right` theorem BddBelow.inter_of_right : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddBelow t → BddBelow (s ∩ t) := by sorry The theorem `BddBelow.inter_of_right` states that, for any type `α` that has a preorder relation, given any two sets `s` and `t` of type `α`, if the set `t` is bounded below, then the intersection of `s` and `t` (denoted as `s ∩ t`) is also bounded below. Thus, the existence of a lower bound for set `t` ensures a lower bound for the intersection of `s` and `t`. More concisely: If `s` and `t` are sets of a preordered type `α` with `t` bounded below, then their intersection `s ∩ t` is also bounded below.
`upperBounds_empty` theorem upperBounds_empty : ∀ {α : Type u} [inst : Preorder α], upperBounds ∅ = Set.univ The theorem `upperBounds_empty` states that for any type `α` that has a preorder relation, the set of upper bounds of the empty set is the universal set. In other words, for any preordered type, every element is considered an upper bound of the empty set, hence the set of all upper bounds for the empty set is the universal set. This makes sense because an upper bound of a set is any element that is greater than or equal to all elements of the set, and since there are no elements in the empty set, all elements of the preordered type trivially satisfy this condition. More concisely: For any preordered type `α`, the set of upper bounds of the empty set is the universal set.
`isGreatest_Iic` theorem isGreatest_Iic : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsGreatest (Set.Iic a) a This theorem states that for any type `α` that has a `Preorder` instance, and for any element `a` of type `α`, `a` is the greatest element of the set of all elements less than or equal to `a`. In other words, in any partially ordered set, an element `a` is considered the greatest in the set of all elements that are less than or equal to `a`. More concisely: For any type `α` with a `Preorder` instance and any `a` in `α`, `a` is the greatest element in the subset of `α` consisting of elements less than or equal to `a`.
`BddAbove.mono` theorem BddAbove.mono : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove s The theorem `BddAbove.mono` states that for any type `α` with a preorder relation, if `s` is a subset of `t` and `t` is bounded above, then `s` is also bounded above. In other words, if every element of `s` is also an element of `t`, and `t` has an upper bound, then `s` must also have an upper bound. More concisely: If a preordered type `α` has a bounded subset `s` that is contained in a bounded subset `t`, then `s` is also bounded.
`mem_upperBounds_image2` theorem mem_upperBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → a ∈ upperBounds s → b ∈ upperBounds t → f a b ∈ upperBounds (Set.image2 f s t) The theorem `mem_upperBounds_image2` states that for all types `α`, `β`, `γ`, which are ordered by preorders, and given a binary function `f: α → β → γ` and sets `s: Set α` and `t: Set β`, if the function `f` is monotone in both of its arguments (the function `f` with one argument fixed is monotone), then for all elements `a` in the upper bounds of `s` and `b` in the upper bounds of `t`, the value `f a b` is in the upper bounds of the image of function `f` over the cartesian product of sets `s` and `t`. This essentially means that if `a` and `b` are upper bounds of sets `s` and `t` respectively, and if `f` is monotone, then `f a b` is an upper bound of the values of `f` taken over all pairs from `s` and `t`. More concisely: If `α`, `β`, `γ` are ordered types, `f: α → β → γ` is a monotone function, `s ⊆ α` and `t ⊆ β`, and `a ∈ upperBound s` and `b ∈ upperBound t`, then `f a b ∈ upperBound (image f (s × t))`.
`IsGreatest.unique` theorem IsGreatest.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGreatest s a → IsGreatest s b → a = b This theorem states that for any set `s` of elements of a given type `α` under a partial order, if `a` and `b` are both greatest elements of `s`, then `a` and `b` must be the same element. In other words, in a partial order, the greatest element of a set, if it exists, is unique. More concisely: In a partial order, if two elements are both maximum elements of a set, then they are equal.
`upperBounds_mono_set` theorem upperBounds_mono_set : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → upperBounds t ⊆ upperBounds s The theorem `upperBounds_mono_set` states that for any type `α` which has a preorder (a reflexive and transitive binary relation), if one set `s` is a subset of another set `t`, then the set of upper bounds of `t` is a subset of the set of upper bounds of `s`. In more detail, an element `x` is an upper bound of a set if each element `a` in the set is less than or equal to `x`. Therefore, if `s` is a subset of `t`, every upper bound for `t` will also be an upper bound for `s`. More concisely: If `α` is a type with a preorder and `s` is a subset of `t`, then the set of upper bounds of `s` is included in the set of upper bounds of `t`.
`not_bddAbove_iff'` theorem not_bddAbove_iff' : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x A set `s` of a certain type `α` is not bounded above if and only if for every element `x` of type `α`, there exists an element `y` in `s` such that `x` is not greater than or equal to `y`. This version of the theorem only assumes a preordered structure and uses the negation of `y ≤ x` notation. There is another version of this theorem for linear orders called `not_bddAbove_iff`. More concisely: A preordered set `s` of type `α` has no upper bound if and only if for every `x` in `α`, there exists `y` in `s` such that `y` is not greater than or equal to `x`. (Equivalently, for all `x`, ∃`y ∈ s`, `y` < `x`.)
`Monotone.map_isLeast` theorem Monotone.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, IsLeast s a → IsLeast (f '' s) (f a) This theorem states that for any types `α` and `β` with preordered structures and a function `f` from `α` to `β`, if `f` is a monotone function, then for any set `s` of type `α` and an element `a` of `α`, if `a` is the least element of `s`, then `f(a)` is the least element of the image of `s` under `f`. In other words, a monotone function preserves the property of being a least element when mapping from one set to another. More concisely: If `f` is a monotone function from preordered types `α` and `β`, then for any set `s` of `α` with least element `a`, `f(a)` is the least element of `f''(s)`.
`Monotone.map_isGreatest` theorem Monotone.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, IsGreatest s a → IsGreatest (f '' s) (f a) The theorem named `Monotone.map_isGreatest` states that for any two types `α` and `β` having the preorder relation, and any monotone function `f` from `α` to `β`, if `a` is the greatest element of a set `s` of type `α`, then `f(a)` is the greatest element of the image of the set `s` under the function `f`. Here, the image of a set `s` under the function `f` is the set of all elements `f(x)` for `x` in `s`. The function `f` is said to be monotone if for all elements `a` and `b` in `α`, `a ≤ b` implies `f(a) ≤ f(b)`. The "greatest" element of a set is one that is in the set and is greater than or equal to all other elements in the set. More concisely: If `a` is the greatest element of a set `s` in a preordered type `α`, and `f` is a monotone function from `α` to another preordered type `β`, then `f(a)` is the greatest element of the image of `s` under `f`.
`IsGLB.of_subset_of_superset` theorem IsGLB.of_subset_of_superset : ∀ {α : Type u} [inst : Preorder α] {a : α} {s t p : Set α}, IsGLB s a → IsGLB p a → s ⊆ t → t ⊆ p → IsGLB t a := by sorry The theorem `IsGLB.of_subset_of_superset` states that if `a` is a greatest lower bound (also known as an infimum) for two sets `s` and `p` in a preordered set `α`, then `a` is also a greatest lower bound for any set `t` that is a subset of `p` and a superset of `s`. This theorem serves as a fundamental property of greatest lower bounds in the context of preorder (or partial order) structures. More concisely: If `a` is the greatest lower bound of sets `s` and `p` in a preordered set `α`, then `a` is also the greatest lower bound of `s ∪ t` for any `t` that is a subset of `p` and `s ⊆ t`.
`Set.Nonempty.bddAbove_lowerBounds` theorem Set.Nonempty.bddAbove_lowerBounds : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, s.Nonempty → BddAbove (lowerBounds s) This theorem states that for any nonempty set `s` of a type `α` equipped with a preorder relation, the set of lower bounds of `s` is bounded above. In other words, if we have at least one element in set `s`, there exists an upper bound for all the lower bounds of `s`. This could be seen as there is a maximum lower bound for `s`. More concisely: For any nonempty set `s` in type `α` with a preorder relation, the set of lower bounds of `s` has a supremum.
`lowerBounds_empty` theorem lowerBounds_empty : ∀ {α : Type u} [inst : Preorder α], lowerBounds ∅ = Set.univ This theorem states that for any type `α` with a preorder (a binary relation that is reflexive and transitive), the set of lower bounds of the empty set is the universal set. In other words, every element of `α` is a lower bound of the empty set. This arises from the vacuous truth property in logic: an implication is always true if its premise is false, and since there are no elements in the empty set, any statement about "all" elements in it is true. More concisely: For any type `α` with a preorder, every element of `α` is a lower bound of the empty set.
`isGLB_Icc` theorem isGLB_Icc : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → IsGLB (Set.Icc a b) a The theorem `isGLB_Icc` states that for any type `α` which has a preorder relation, and any two elements `a` and `b` of type `α` such that `a` is less than or equal to `b`, `a` is the greatest lower bound of the closed interval from `a` to `b`. In other words, for any element `x` in the closed interval `[a, b]`, `a` is less than or equal to `x`. It should be noted that the notion of a "closed interval" is generalized for any preorder and not just the standard order on real numbers. More concisely: For any type `α` with a preorder relation and any `a, b ∈ α` with `a ≤ b`, `a` is the greatest lower bound of the interval `[a, b]` if and only if `a ≤ x` for all `x ∈ [a, b]`.
`IsLeast.isGLB` theorem IsLeast.isGLB : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → IsGLB s a This theorem states that for any set `s` of a type `α` with a preorder (a binary relation that is reflexive and transitive), if an element `a` from `α` is the least element of `s`, then `a` is also the greatest lower bound of `s`. In other words, if `a` is in `s` and no element in `s` is less than `a`, then `a` is the highest possible value that is less than or equal to every element in `s`. More concisely: If a preorder `≤` on a set `α` has a least element `a` in `s ≤ α`, then `a` is the greatest lower bound of `s`.
`mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds` theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Antitone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → a ∈ upperBounds s → b ∈ lowerBounds t → f a b ∈ lowerBounds (Set.image2 f s t) The theorem `mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds` is a statement about a binary function `f : α → β → γ`, two sets `s : Set α` and `t : Set β`, and two elements `a : α` and `b : β`, where the types α, β, γ are equipped with preorder structures. It states that if every function obtained by fixing the second argument of `f` is antitone (i.e., decreases when its argument increases), every function obtained by fixing the first argument of `f` is monotone (i.e., increases when its argument increases), `a` is an upper bound of set `s`, and `b` is a lower bound of set `t`, then the value `f a b` is a lower bound of the image of the sets `s` and `t` under the function `f`. This can be thought of as a property relating the bounds of the original sets `s` and `t` to the bounds of their image under `f`. More concisely: If functions obtained by fixing the arguments of a binary function are antitone on the second argument and monotone on the first, and elements `a` from the domain of the first argument and `b` from the domain of the second argument are upper and lower bounds of their respective sets, then `f(a, b)` is a lower bound for the images of those sets under `f`.
`Monotone.mem_upperBounds_image` theorem Monotone.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, a ∈ upperBounds s → f a ∈ upperBounds (f '' s) This theorem states that for any types `α` and `β` with preorder relations, and any monotone function `f` from `α` to `β`, if an element `a` is in the upper bounds of a set `s` of type `α`, then `f(a)` is in the upper bounds of the image of the set `s` under the function `f`. In other words, if `a` is an upper bound of `s`, then `f(a)` is an upper bound of `f(s)`. This theorem encapsulates the property of monotone functions to preserve the order relationship between elements and sets under the operation of taking upper bounds. More concisely: For any monotonic function $f$ from preordered types $\alpha$ and $\beta$, if $a$ is an upper bound of a set $s$ in $\alpha$, then $f(a)$ is an upper bound of $f(s)$ in $\beta$.
`mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds` theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Antitone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → a ∈ lowerBounds s → b ∈ upperBounds t → f a b ∈ upperBounds (Set.image2 f s t) This theorem states that for all types `α`, `β`, and `γ` that have a `Preorder` relation, and for any function `f` from `α` and `β` to `γ`, given a set `s` of type `α` and a set `t` of type `β`, if the function `f` is antitone with respect to `b` when its arguments are swapped, and is monotone with respect to `a`, and if `a` is a lower bound of set `s` and `b` is an upper bound of set `t`, then the value `f a b` is an upper bound of the image of function `f` over the Cartesian product of sets `s` and `t`. In other words, `f a b` is greater than or equal to all elements in the image of `f` over all pairs `(x, y)` where `x` is from set `s` and `y` is from set `t`. More concisely: For any antitone and monotone function `f` between two preordered sets `α × β` with `α`'s lowest element `a` as a lower bound of set `s` and `β`'s upper bound `b` as an upper bound of set `t`, `f a b` is an upper bound of `f(s × t)`.
`AntitoneOn.map_isLeast` theorem AntitoneOn.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α}, AntitoneOn f t → ∀ {a : α}, IsLeast t a → IsGreatest (f '' t) (f a) The theorem `AntitoneOn.map_isLeast` states that for any types `α` and `β` that are preordered, any function `f` from `α` to `β`, and any set `t` of type `α`, if the function `f` is antitone on the set `t` (meaning that for all elements `a` and `b` in `t`, if `a ≤ b`, then `f(b) ≤ f(a)`), then for any element `a` that is the least element of the set `t`, `f(a)` is the greatest element of the image of `t` under `f`. In other words, an antitone map sends the least element of a set to the greatest element of its image. More concisely: If `f` is an antitone function from a preordered set `α` to a preordered set `β`, and `a` is the least element of a set `t` in `α`, then `f(a)` is the greatest element of `f``(t)`.
`Monotone.mem_lowerBounds_image` theorem Monotone.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, a ∈ lowerBounds s → f a ∈ lowerBounds (f '' s) The theorem `Monotone.mem_lowerBounds_image` states that for every types `α` and `β` that have a preorder, and for any function `f` from `α` to `β` that is monotone, if an element `a` from `α` is in the lower bounds of a set `s` of `α`, then `f(a)` is in the lower bounds of the image of `s` under `f`. In other words, if a function is monotone and an element is a lower bound of a set, then the image of that element under the function is a lower bound of the image of the set under the function. More concisely: If `f` is a monotone function from preordered types `α` and `β`, and `a` is a lower bound of a set `s` in `α`, then `f(a)` is a lower bound of the image of `s` under `f` in `β`.
`not_bddAbove_iff` theorem not_bddAbove_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y The theorem `not_bddAbove_iff` states that for any set `s` of a certain type `α` which is equipped with a linear order, `s` is not bounded above if and only if, for every element `x` of type `α`, there exists an element `y` in `s` such that `y` is strictly greater than `x`. In other words, no matter how high you choose `x`, you can always find an element in the set `s` that surpasses it, hence `s` is not bounded above. This version of the theorem is specifically for structures with a linear order. More concisely: A set equipped with a linear order is unbounded if and only if for every element x in the set, there exists a y in the set strictly greater than x.
`isGreatest_univ` theorem isGreatest_univ : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α], IsGreatest Set.univ ⊤ This theorem, `isGreatest_univ`, states that for any type `α` that has a preorder and is also an ordered set with a maximum element (denoted as `⊤`), the maximum element is the greatest element of the universal set (i.e., the set that contains all elements of `α`). In other words, no element in the universal set of `α` is greater than the maximum element `⊤`. More concisely: For any type `α` with a preorder and a maximum element `⊤`, the maximum element is the greatest element in the universal set of `α`. (i.e., for all `x ∈ α`, `x ≤ ⊤`).
`IsGLB.dual` theorem IsGLB.dual : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a) The theorem `IsGLB.dual` states that for any type `α` with a pre-order relation, any set `s` of elements of type `α`, and any element `a` of type `α`, if `a` is a greatest lower bound of the set `s`, then the dual of `a` is the least upper bound of the dual of the set `s`. The `OrderDual.ofDual` function is used to map elements from the original order to the dual order and `OrderDual.toDual` is used to map `a` to its dual. Essentially, it is stating that taking the dual of a pre-order reverses the order of the bounds. More concisely: For any pre-order type `α` and set `s` of elements, if `a` is the greatest lower bound of `s`, then the dual of `a` is the least upper bound of the dual of `s`.
`BddBelow.mono` theorem BddBelow.mono : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddBelow t → BddBelow s This theorem states that if a set `s` of a certain type `α` (with a preorder relation defined) is a subset of another set `t`, and if `t` has a lower bound, then `s` also has a lower bound. This is a theorem about the transfer of the property of being bounded below between subsets, in the context of preordered sets. More concisely: If `s` is a subset of preordered set `t` with a lower bound, then `s` also has a lower bound.
`BddAbove.inter_of_right` theorem BddAbove.inter_of_right : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddAbove t → BddAbove (s ∩ t) := by sorry This theorem states that for any two sets `s` and `t` of a type `α` that has a preorder relation, if `t` is a bounded set, then their intersection `s ∩ t` is also a bounded set. In other words, if there exists an upper bound for the set `t`, then there also exists an upper bound for the intersection of `s` and `t`. More concisely: If `α` is a type with a preorder relation, and `t` is a bounded subset of `α` with an upper bound, then `s ∩ t` is also a bounded subset of `α`.
`IsGLB.exists_between` theorem IsGLB.exists_between : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → a < b → ∃ c ∈ s, a ≤ c ∧ c < b This theorem states that for any type `α` equipped with a `LinearOrder`, given a set `s` of type `α` and two elements `a` and `b` of type `α`, if `a` is a greatest lower bound (GLB) of the set `s` and `a` is less than `b`, then there exists an element `c` in set `s` such that `a` is less than or equal to `c` and `c` is less than `b`. In other words, whenever `a` is a GLB of a set and `a` is strictly less than `b`, we can always find an element in the set that lies between `a` and `b`. More concisely: If `α` is a type with a `LinearOrder`, `s` is a non-empty subset of `α`, `a` is the greatest lower bound of `s`, and `a` is strictly less than `b` in `α`, then there exists `c` in `s` such that `a ≤ c` and `c < b`.
`OrderBot.bddBelow` theorem OrderBot.bddBelow : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] (s : Set α), BddBelow s This theorem states that, given any type `α` with a preorder and a global minimum (denoted by `OrderBot α`), every set of elements of type `α` is bounded below. In other words, for any set `s` of elements from a type `α` that has a predefined order and a lowest possible value, there exists at least one element in `α` that is less than or equal to every element in `s`. This element represents a lower bound of the set `s`. More concisely: Given a preordered type `α` with a global minimum `OrderBot α`, every subset of `α` has a least lower bound.
`bddAbove_Iio` theorem bddAbove_Iio : ∀ {α : Type u} [inst : Preorder α] {a : α}, BddAbove (Set.Iio a) The theorem `bddAbove_Iio` states that for any type `α` with a pre-order relation, and for any element `a` of type `α`, the left-infinite right-open interval `(,a)` (denoted as `Set.Iio a` in Lean) is always bounded above. In other words, there exists an upper bound for all elements `x` such that `x < a`. More concisely: For any type `α` with a pre-order relation and any element `a` in `α`, the left-infinite right-open interval `(,a)` has an upper bound.
`Monotone.map_bddBelow` theorem Monotone.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, BddBelow s → BddBelow (f '' s) The theorem states that the image of a set, which is bounded below, under a monotone function, is also bounded below. In other words, if there is a monotone function `f` from type `α` to type `β`, and if there exists a set `s` of type `α` that is bounded below, then the image of the set `s` through the function `f` is also bounded below. Here, both types `α` and `β` are preordered, meaning that they possess a binary relation indicating that, for any two elements in the set, one of the elements is less than or equal to the other. More concisely: If `f` is a monotone function from preordered set `α` to preordered set `β`, and `s ⊆ α` has a bottom element, then `f''s` has a bottom element.
`AntitoneOn.map_bddAbove` theorem AntitoneOn.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, AntitoneOn f t → s ⊆ t → (upperBounds s ∩ t).Nonempty → BddBelow (f '' s) The theorem `AntitoneOn.map_bddAbove` states that for any set `s` that is a subset of `t` and any antitone function `f` defined on `t` (i.e., a function for which if `a ≤ b`, then `f(b) ≤ f(a)` for all `a, b ∈ t`), if `s` has an upper bound in `t`, then the image of `s` under `f` is bounded below. In other words, applying an antitone function to a set that is bounded above results in a set that is bounded below. More concisely: If `s` is a subset of `t` with an upper bound, and `f` is an antitone function on `t`, then the image of `s` under `f` has a lower bound.
`BddAbove.inter_of_left` theorem BddAbove.inter_of_left : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddAbove s → BddAbove (s ∩ t) := by sorry The theorem `BddAbove.inter_of_left` states that for any type `α` that has a preorder relationship, if a set `s` of type `α` is bounded above, then the intersection of `s` and another set `t` of type `α` is also bounded above. In simpler terms, if we have an upper bound for a set `s`, then the intersection of `s` with any other set `t` will also have an upper bound. More concisely: If `s` and `t` are bounded above in a preordered type `α`, then their intersection `s ∩ t` is also bounded above.
`IsGLB.lowerBounds_eq` theorem IsGLB.lowerBounds_eq : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → lowerBounds s = Set.Iic a The theorem `IsGLB.lowerBounds_eq` states that for any set `s` of a certain type `α`, under a preorder relation, and any element `a` of type `α`, if `a` is the greatest lower bound of `s`, then the set of lower bounds of `s` is equal to the left-infinite right-closed interval up to `a`. In other words, all elements that are less than or equal to `a` form the set of lower bounds of `s` when `a` is the greatest lower bound of `s`. More concisely: If `a` is the greatest lower bound of a set `s`, then the set of lower bounds of `s` equals the set of all elements less than or equal to `a`.
`IsGLB.unique` theorem IsGLB.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGLB s a → IsGLB s b → a = b := by sorry This theorem states that for any type `α` with a partial order, and any set `s` of type `α`, if `a` and `b` are both greatest lower bounds of the set `s`, then `a` must be equal to `b`. In other words, the greatest lower bound of a set in a partial order is unique if it exists. This follows from the antisymmetry of the partial order. More concisely: In a partial order, if two elements are both the greatest lower bounds of a set, then they are equal.
`isLUB_le_iff` theorem isLUB_le_iff : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a b : α}, IsLUB s a → (a ≤ b ↔ b ∈ upperBounds s) The theorem `isLUB_le_iff` states that for any type `α` with a preorder, and for any sets `s` of elements of type `α` and any elements `a` and `b` of type `α`, if `a` is a least upper bound of the set `s`, then `a` is less than or equal to `b` if and only if `b` is an upper bound of the set `s`. In other words, any element that is greater than or equal to the least upper bound of a set is itself an upper bound of that set. More concisely: If `a` is the least upper bound of a set `s` in a preordered type `α`, then `a` is less than or equal to every upper bound `b` of `s`.
`Monotone.image_upperBounds_subset_upperBounds_image` theorem Monotone.image_upperBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, f '' upperBounds s ⊆ upperBounds (f '' s) This theorem states that for any types `α` and `β` equipped with a preorder (a relation that is reflexive and transitive), and any function `f` from `α` to `β`, if `f` is monotone (i.e., preserves the order: `a ≤ b` implies `f a ≤ f b`), then for any set `s` of type `α`, the image under `f` of the upper bounds of `s` is a subset of the upper bounds of the image of `s` under `f`. In other words, if `f` preserves order and `x` is an upper bound of `s`, then `f(x)` is an upper bound of `f(s)`. More concisely: For any function `f` that preserves the order between elements of types `α` and `β`, where `α` and `β` are equipped with a preorder, and for any set `s` of type `α` and any upper bound `x` of `s`, the image `f(x)` is an upper bound of `f(s)`.
`isLUB_Ico` theorem isLUB_Ico : ∀ {γ : Type w} [inst : SemilatticeInf γ] [inst_1 : DenselyOrdered γ] {a b : γ}, a < b → IsLUB (Set.Ico a b) b := by sorry The theorem `isLUB_Ico` states that for any type `γ` with a semilattice structure and a densely ordered structure, and for any two elements `a` and `b` of `γ` such that `a < b`, the element `b` is a least upper bound of the left-closed right-open interval from `a` to `b` (denoted as `[a, b)`). In other words, `b` is the smallest element that is greater than or equal to every element in the interval `[a, b)`. More concisely: For any semilattice and densely ordered type `γ` with elements `a` and `b` such that `a < b`, the element `b` is the least upper bound of the interval `[a, b)`.
`bddAbove_insert` theorem bddAbove_insert : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] {s : Set α} {a : α}, BddAbove (insert a s) ↔ BddAbove s The theorem `bddAbove_insert` states that for any type `α` that has a preorder structure and is directed (meaning, for any two elements `x` and `x_1` of `α`, there exists another element of `α` that is greater than or equal to both `x` and `x_1`), and for any set `s` of elements of `α` and an element `a` of `α`, adding the element `a` to the set `s` preserves its property of being bounded above. In other words, if a set is bounded above, then adding any element to this set will still keep it bounded above. More concisely: For any directed type `α` with a preorder structure and any set `s` of elements of `α` bounded above, the set `s ∪ {a}` is also bounded above for any `a` in `α`.
`mem_lowerBounds_image2` theorem mem_lowerBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → a ∈ lowerBounds s → b ∈ lowerBounds t → f a b ∈ lowerBounds (Set.image2 f s t) This theorem states that for any types `α`, `β`, and `γ` that are preordered, given a binary function `f` from `α` and `β` to `γ`, and two sets `s` of type `α` and `t` of type `β`, if the function `f` is monotone when the second argument is fixed (as expressed by `∀ (b : β), Monotone (Function.swap f b)`) and is also monotone when the first argument is fixed (as expressed by `∀ (a : α), Monotone (f a)`), then for any `a` in the lower bounds of `s` and any `b` in the lower bounds of `t`, `f a b` is in the lower bounds of the image of the function `f` from `s` to `t` (denoted by `Set.image2 f s t`). In simpler terms, this theorem demonstrates the preservation of lower bounds under the image of a binary monotone function. More concisely: If `f` is a binary monotone function from preordered types `α`, `β`, and `γ`, then for any sets `s` of type `α` and `t` of type `β` with lower bounds `a` in `s` and `b` in `t`, `f a b` is in the lower bounds of `Set.image2 f s t`.
`mem_upperBounds_image2_of_mem_lowerBounds` theorem mem_upperBounds_image2_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Antitone (Function.swap f b)) → (∀ (a : α), Antitone (f a)) → a ∈ lowerBounds s → b ∈ lowerBounds t → f a b ∈ upperBounds (Set.image2 f s t) This theorem states that for any types `α`, `β`, `γ`, where `α`, `β`, `γ` each have a preorder, given a function `f` from `α` and `β` to `γ`, sets `s` and `t` of `α` and `β` respectively, and elements `a` in `α` and `b` in `β`, if for all `b` in `β`, the function obtained by fixing `b` and varying the other argument of `f` is antitone (i.e., it reverses the order), and similarly, for all `a` in `α`, the function obtained by fixing `a` and varying the other argument of `f` is antitone, and if `a` is a lower bound of `s` and `b` is a lower bound of `t`, then the value `f(a, b)` is an upper bound of the image of the set `s × t` under `f`. More concisely: If functions `f` from a preordered type `α` to a preordered type `γ` with antitone components for every element, and `a` is a lower bound of a set `s` in `α` and `b` is a lower bound of set `t` in `β`, then `f(a, b)` is an upper bound of the image of `s × t` under `f`.
`MonotoneOn.mem_lowerBounds_image` theorem MonotoneOn.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, MonotoneOn f t → ∀ {a : α}, s ⊆ t → a ∈ lowerBounds s → a ∈ t → f a ∈ lowerBounds (f '' s) The theorem `MonotoneOn.mem_lowerBounds_image` states that for any types `α` and `β` with preorder structures, any function `f: α → β`, and any sets `s` and `t` of `α`, if `f` is monotone on `t`, and `s` is a subset of `t`, then for any element `a` of `α`, if `a` is a lower bound of `s` and `a` is in `t`, then `f(a)` is a lower bound of the image of `s` under `f`. In other words, if a function is monotone on a set, then it preserves the property of being a lower bound when it maps elements of a subset of that set. More concisely: If `f: α → β` is a monotone function on a set `t subseteq α`, and `a` is a lower bound of `s subseteq t` in `α`, then `f(a)` is a lower bound of the image of `s` under `f` in `β`.
`OrderTop.bddAbove` theorem OrderTop.bddAbove : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] (s : Set α), BddAbove s The theorem `OrderTop.bddAbove` states that for any type `α` that has a preorder and an order top (a greatest element), every set of this type is bounded above. In other words, for any set `s` of elements of such type `α`, there exists an element in `α` that is greater than or equal to every element in `s`. This holds true because the existence of a global maximum (the order top) serves as an upper bound for all sets. More concisely: For any type equipped with a preorder and an order top, every subset has an upper bound.
`MonotoneOn.mem_upperBounds_image` theorem MonotoneOn.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, MonotoneOn f t → ∀ {a : α}, s ⊆ t → a ∈ upperBounds s → a ∈ t → f a ∈ upperBounds (f '' s) The theorem `MonotoneOn.mem_upperBounds_image` states that for all types `α` and `β` having a preorder, for any function `f` from `α` to `β`, and any sets `s` and `t` of type `α`, if the function `f` is monotone on `t`, and given `s` is a subset of `t`, if any element `a` is an upper bound of `s` and also belongs to `t`, then the image of `a` under `f` is an upper bound of the image of `s` under `f`. In other words, if a function is monotone on a set `t`, then the image under this function of an upper bound of any subset of `t` is an upper bound of the image of this subset. More concisely: If `f` is a monotone function from `α` to `β`, and `s` is a subset of `t` in `α` such that `a` is an upper bound of `s` and belongs to `t`, then the image `f(a)` is an upper bound of the image `f(s)`.
`isLeast_Ici` theorem isLeast_Ici : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsLeast (Set.Ici a) a This theorem states that for any given type `α` that has a preorder defined on it, and any element `a` of type `α`, `a` is a least element of the set of all elements `x` such that `a` is less than or equal to `x`. In mathematical terms, given a set `S` defined as {x \| a ≤ x}, `a` is both a member of `S` and a lower bound for `S` under the given preorder. More concisely: For any type `α` with a preorder and any element `a` of `α`, `a` is the least element of the set `{x : α \| a ≤ x}` under the given preorder.
`isGLB_Ioo` theorem isGLB_Ioo : ∀ {γ : Type w} [inst : SemilatticeSup γ] [inst_1 : DenselyOrdered γ] {a b : γ}, a < b → IsGLB (Set.Ioo a b) a := by sorry The theorem `isGLB_Ioo` states that for any type `γ` that is both a semilattice with sup operation and densely ordered, and for any two elements `a` and `b` of this type such that `a` is less than `b`, `a` is the greatest lower bound (GLB) of the open interval between `a` and `b`. This means that `a` is less than or equal to every element in the open interval from `a` to `b` (`a` and `b` excluded), and any other element that is also less than or equal to every element of the interval is less than or equal to `a`. More concisely: For any semilattice `γ` with sup operation and dense ordering, if `a` is the least element greater than or equal to `a` in the open interval `(a, b)`, then `a` is the greatest lower bound of `(a, b)`.
`le_isGLB_iff` theorem le_isGLB_iff : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a b : α}, IsGLB s a → (b ≤ a ↔ b ∈ lowerBounds s) This theorem states that for all sets `s` of some type `α` with defined preorder, and any elements `a` and `b` of type `α`, if `a` is the greatest lower bound of the set `s`, then `b` is less than or equal to `a` if and only if `b` belongs to the set of lower bounds of `s`. In terms of mathematical language, we can denote the greatest lower bound as $\text{glb}(s) = a$, and the theorem states $b \leq a \iff b \in \text{lowerBounds}(s)$. More concisely: The greatest lower bound of a set with respect to a preorder is an element that is less than or equal to any lower bound of the set. In other words, $\text{glb}(s) = a \iff a \leq b \ \forall\ b \in \text{lowerBounds}(s)$.
`mem_upperBounds` theorem mem_upperBounds : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a This theorem establishes a membership criterion for the set of upper bounds of a given set in a preordered type. Specifically, it states that for any type `α` equipped with a preorder, a set `s : Set α`, and an element `a : α`, `a` is an upper bound of `s` if and only if for every element `x` in `s`, `x` is less than or equal to `a`. This means that `a` is an upper bound of `s` if it is greater than or equal to all elements of `s`. More concisely: For any preordered type `α`, set `s : Set α`, and element `a : α`, `a` is an upper bound of `s` if and only if `x ≤ a` for all `x ∈ s`.
`IsGLB.of_image` theorem IsGLB.of_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) → ∀ {s : Set α} {x : α}, IsGLB (f '' s) (f x) → IsGLB s x This theorem states that for any two types `α` and `β` with preorder (a reflexive and transitive binary relation) structures, and a function `f` from `α` to `β`, if the function `f` preserves the preorder (meaning if `f x` is less than or equal to `f y` if and only if `x` is less than or equal to `y`), then for any set `s` of elements of type `α` and an element `x` of type `α`, if `f x` is the greatest lower bound of the image of the set `s` under the function `f`, then `x` is the greatest lower bound of the set `s`. In other words, if `f x` is the largest value that is less than or equal to all elements in the image of `s` under `f`, then `x` itself is the largest value that is less than or equal to all elements in `s`. More concisely: If `f` is a function from preordered types `α` to `β` that preserves the preorder, and `x` is the greatest lower bound of `s ↦ f(s)` in `β`, then `x` is the greatest lower bound of `s` in `α`.
`isGLB_singleton` theorem isGLB_singleton : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsGLB {a} a This theorem states that for any type `α` equipped with a preorder, and for any element `a` of `α`, `a` is the greatest lower bound of the singleton set containing just `a`. In other words, if we consider the set that contains only the element `a`, there does not exist any lower bound which is strictly greater than `a`. More concisely: For any preordered type `α` and its element `a`, `a` is the greatest lower bound of the singleton set `{a}`.
`bddAbove_range_prod` theorem bddAbove_range_prod : ∀ {ι : Sort x} {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {F : ι → α × β}, BddAbove (Set.range F) ↔ BddAbove (Set.range (Prod.fst ∘ F)) ∧ BddAbove (Set.range (Prod.snd ∘ F)) This theorem states that for any function `F` from a type `ι` to a product of types `α` and `β` (where `α` and `β` have pre-order relations), the range of `F` is bounded above if and only if both the range of the first projection of `F` and the range of the second projection of `F` are bounded above. In other words, a set of ordered pairs is bounded above if and only if the set of all first components of the pairs and the set of all second components of the pairs are both bounded above. More concisely: The range of a function from a type to a product of types, each with a preorder relation, is bounded above if and only if the ranges of both projections are bounded above.
`isLeast_singleton` theorem isLeast_singleton : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsLeast {a} a The theorem `isLeast_singleton` states that for any type `α` that has a Preorder (a type of partial order), and for any element `a` of this type, `a` is a least element of the singleton set `{a}`. In other words, `a` is both a member of the set `{a}` and a lower bound of the set `{a}` in the given preorder. More concisely: For any type `α` with a preorder and any element `a` in `α`, `a` is the least element of the singleton set `{a}`.
`IsLUB.unique` theorem IsLUB.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLUB s a → IsLUB s b → a = b := by sorry This theorem states that for any type `α` equipped with a partial order and for any set `s` of elements of type `α`, if both `a` and `b` are least upper bounds of the set `s`, then `a` and `b` must be equal. In mathematical terms, in a partially ordered set, the least upper bound of a given set, if it exists, is unique. More concisely: In a partially ordered set, if two elements are the least upper bounds of a set, then they are equal.
`Antitone.map_isLeast` theorem Antitone.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Antitone f → ∀ {a : α} {s : Set α}, IsLeast s a → IsGreatest (f '' s) (f a) The theorem `Antitone.map_isLeast` states that for any antitone function `f` (a function that inverts the order: if `a ≤ b`, then `f(b) ≤ f(a)`), if `a` is the least element of a set `s`, then `f(a)` is the greatest element of the image of `s` under `f`. In other words, an antitone function maps the least element of a set to the greatest element of its image. This holds for any types `α` and `β` that have a preorder (a relation that is reflexive and transitive), and any set `s` of elements of type `α`. More concisely: For any antitone function $f$ between preordered types $\alpha$ and $\beta$, if $a$ is the least element of a set $s$ in $\alpha$, then $f(a)$ is the greatest element of $f(s)$.
`upperBounds_mono_mem` theorem upperBounds_mono_mem : ∀ {α : Type u} [inst : Preorder α] {s : Set α} ⦃a b : α⦄, a ≤ b → a ∈ upperBounds s → b ∈ upperBounds s The theorem `upperBounds_mono_mem` asserts that for any given type `α` that has a preorder relation and a set `s` of this type, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b` and `a` is an upper bound of `s`, then `b` is also an upper bound of `s`. In other words, if `a` is an element that is greater than or equal to every element in `s` and `b` is greater than or equal to `a`, then `b` must also be greater than or equal to every element in `s`. More concisely: If `a` is an upper bound of a preordered set `s` and `a` is less than or equal to `b`, then `b` is also an upper bound of `s`.
`IsGLB.bddBelow` theorem IsGLB.bddBelow : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → BddBelow s The theorem `IsGLB.bddBelow` states that for any type `α` that has a preorder relation, if a set `s` of type `α` has a greatest lower bound `a`, then the set `s` is bounded below. In other words, if there exists an element `a` in the set `s` such that no other element in `s` is lower than `a`, then there exists at least one element in `s` that acts as a lower bound. More concisely: If a preordered set `α` with greatest lower bound `a` in `s ⊆ α` exists, then `s` is non-empty and has a lower bound.
`AntitoneOn.map_isGreatest` theorem AntitoneOn.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α}, AntitoneOn f t → ∀ {a : α}, IsGreatest t a → IsLeast (f '' t) (f a) The theorem `AntitoneOn.map_isGreatest` states that for any given preorder sets `α` and `β`, if a function `f` is antitone on a set `t` (i.e., for all `a, b` in `t`, `a ≤ b` implies `f(b) ≤ f(a)`), and if `a` is the greatest element in set `t`, then `f(a)` is the least element in the image set `f '' t`. In essence, an antitone mapping transforms the greatest element of a set into the least element of its image set. More concisely: If `f` is an antitone function from a preorder set `α` to another preorder set `β`, and `a` is the greatest element in `α` with respect to the preorder relation, then `f(a)` is the least element in the image `f''α` with respect to the preorder relation in `β`.
`Mathlib.Order.Bounds.Basic._auxLemma.21` theorem Mathlib.Order.Bounds.Basic._auxLemma.21 : ∀ {α : Type u} [inst : Preorder α] [inst_1 : Nonempty α], BddAbove ∅ = True This theorem states that for any given type `α` and any preorder `inst` on this type, if `α` is nonempty, then the empty set is bounded above. In other words, there exists an upper bound for the empty set under these conditions. More concisely: For any nonempty type `α` and preorder `≤` on `α`, the empty set is bounded above.
`MonotoneOn.map_isLeast` theorem MonotoneOn.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α}, MonotoneOn f t → ∀ {a : α}, IsLeast t a → IsLeast (f '' t) (f a) The theorem `MonotoneOn.map_isLeast` states that, given a set `t` of elements of some type `α` and a function `f` from `α` to another type `β`, both `α` and `β` being equipped with a preorder relation, if `f` is monotone on `t` and `a` is a least element of `t`, then the image of `a` under `f` is a least element of the image of `t` under `f`. In other words, if a function preserves the order of elements (is monotone) and is applied onto a least element in a set, the result is the least element in the image set. More concisely: If `f` is a monotone function from a preordered set `(α, ≤)` to another preordered set `(β, ≤)` and `a` is the least element of `{x : α \| x ∈ t}`, then `f(a)` is the least element of `{f(x) : β \| x ∈ t}`.
`BddBelow.union` theorem BddBelow.union : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] {s t : Set α}, BddBelow s → BddBelow t → BddBelow (s ∪ t) In the context of a preordered type `α` that is additionally a codirected order (i.e., for any two elements, there exists a common lower bound), the theorem `BddBelow.union` states that if two sets `s` and `t` of this type `α` are both bounded below (i.e., each set has at least one element that is less than or equal to all others in the set), then the union of these two sets is also bounded below. More concisely: If `α` is a preordered type with the property that every two elements have a common lower bound, and `s` and `t` are subsets of `α` that are bounded below, then their union `s ∪ t` is also bounded below.
`BddBelow.image2` theorem BddBelow.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → BddBelow s → BddBelow t → BddBelow (Set.image2 f s t) The given theorem, `BddBelow.image2`, states that for any types `α`, `β`, and `γ` with preorder relations, a binary function `f : α → β → γ`, and sets `s : Set α` and `t : Set β`, if the function `f` when fixed with any `b : β` is monotone in `α`, and `f` when fixed with any `a : α` is monotone in `β`, and if both sets `s` and `t` are bounded below, then the set formed by the image of the binary function `f` on sets `s` and `t`, denoted as `Set.image2 f s t`, is also bounded below. This means that when `f` is monotone and both input sets have lower bounds, the resulting set of all possible values of `f` also has a lower bound. More concisely: If functions `f : α → β → γ`, `s : Set α`, and `t : Set β` satisfy `f` is monotone in `α` for all `b : β` and monotone in `β` for all `a : α`, and `s` and `t` have lower bounds, then `Set.image2 f s t` also has a lower bound.
`mem_lowerBounds` theorem mem_lowerBounds : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x The theorem `mem_lowerBounds` states that for any type `α` with a preorder (i.e., a relation satisfying reflexivity and transitivity) and for any set `s` of type `α` and element `a` of type `α`, `a` is in the lower bounds of `s` if and only if `a` is less than or equal to every element `x` in `s`. In other words, an element is considered a lower bound of a set in a preorder if it is less than or equal to every element of the set. More concisely: An element is a lower bound of a set in a preorder if and only if it is less than or equal to every element in the set.
`IsGreatest.bddAbove` theorem IsGreatest.bddAbove : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → BddAbove s := by sorry The theorem `IsGreatest.bddAbove` asserts that for any set `s` of a certain type `α` within a preorder, if `s` has a greatest element `a`, then `s` is bounded above. In other words, if there exists a greatest element `a` within a set `s`, then there also exists an upper bound for the set `s`. This conclusion holds for all preorders, which are reflexive and transitive binary relations, and for all types `α`. More concisely: In any preorder, if a set has a greatest element, then it is bounded above.
`isGLB_lt_iff` theorem isGLB_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → (a < b ↔ ∃ c ∈ s, c < b) This theorem states that for any type `α` that is a linear order, and for any set `s` of type `α` and any two elements `a` and `b` of type `α`, if `a` is a greatest lower bound of set `s`, then `a` is less than `b` if and only if there exists an element `c` in set `s` that is less than `b`. In other words, a greatest lower bound of a set is less than another quantity if and only if there's a member in the set that is also less than this quantity. This theorem is a key property that characterizes greatest lower bounds in the context of linear orders. More concisely: For any linear order type `α`, any set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `a` is the greatest lower bound of `s`, then `a < b` if and only if there exists `c` in `s` such that `c < b`.
`mem_lowerBounds_image2_of_mem_upperBounds` theorem mem_lowerBounds_image2_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Antitone (Function.swap f b)) → (∀ (a : α), Antitone (f a)) → a ∈ upperBounds s → b ∈ upperBounds t → f a b ∈ lowerBounds (Set.image2 f s t) The theorem `mem_lowerBounds_image2_of_mem_upperBounds` states that for all types `α`, `β`, `γ` with preorder relations, a binary function `f : α → β → γ`, and sets `s` of type `α` and `t` of type `β`, if `f` is antitone with respect to both its arguments, then for any elements `a` in the upper bounds of `s` and `b` in the upper bounds of `t`, the image of `f` applied to `a` and `b` is in the lower bounds of the image of the binary function `f` applied to sets `s` and `t`. In simple words, if `f` reverses the order of its arguments and `a` and `b` are upper bounds of their respective sets, then `f(a, b)` is a lower bound of the set of all possible values of `f` when applied to elements of sets `s` and `t`. More concisely: If `f : α → β → γ` is an antitone function between preordered sets `(α, ≤α)` and `(β, ≤β)`, and `a ∈ ⨆ s` and `b ∈ ⨆ t`, then `f a b ∈ ⊓ (f '' s) ∩ (f '' t)`. (Here, `s ⊆ α`, `t ⊆ β`, `s''` denotes the image of `s` under `f`, and `⨆` and `⊓` represent the upper bounds and lower bounds of sets, respectively.)
`bddBelow_Icc` theorem bddBelow_Icc : ∀ {α : Type u} [inst : Preorder α] {a b : α}, BddBelow (Set.Icc a b) This theorem states that for any type `α` that has a preorder, and for any two elements `a` and `b` of this type `α`, the closed interval from `a` to `b` (i.e., the set of all elements `x` such that `a ≤ x ≤ b`) is bounded below. In simpler terms, there exists at least one element in `α` that is less than or equal to all elements in the interval from `a` to `b`. More concisely: For any preorder type `α` and elements `a` and `b` in `α`, there exists an element `c` in `α` such that `a ≤ c` and `c ≤ b`.
`Antitone.map_bddAbove` theorem Antitone.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Antitone f → ∀ {s : Set α}, BddAbove s → BddBelow (f '' s) The theorem `Antitone.map_bddAbove` states that for any type `α` and `β` that have a preorder relation, and any function `f` from `α` to `β`, if `f` is an antitone function (meaning if `a ≤ b` then `f b ≤ f a`), and if a set `s` of type `α` is bounded above (meaning there exists an upper bound for `s`), then the image of the set `s` under the function `f` is bounded below (meaning there exists a lower bound for the image of `s` under `f`). In mathematical terms, if ∃M such that ∀x∈s, x≤M, then ∃m such that ∀y∈f(s), m≤y. More concisely: If `α` and `β` have a preorder relation, `f: α → β` is antitone, and `s ⊆ α` has an upper bound, then `f(s)` has a lower bound.
`IsLeast.unique` theorem IsLeast.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLeast s a → IsLeast s b → a = b The theorem `IsLeast.unique` states that for any type `α` equipped with a partial order, a set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `a` and `b` are both least elements of the set `s` (i.e., each belongs to `s` and is a lower bound of `s`), then `a` and `b` must be equal. This corresponds to the uniqueness property of the least element in a partially ordered set. More concisely: In a partially ordered set, if two elements are both the least elements, then they are equal.
`BddBelow.inter_of_left` theorem BddBelow.inter_of_left : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddBelow s → BddBelow (s ∩ t) := by sorry The theorem `BddBelow.inter_of_left` states that for any type `α` that has a preorder structure and for any two sets `s` and `t` of type `α`, if the set `s` is bounded below, then the intersection of `s` and `t`, denoted as `s ∩ t`, is also bounded below. In other words, if there exists a lower bound for the elements of `s`, then such a lower bound also exists for the elements that are common to both `s` and `t`. More concisely: If `s` and `t` are sets of a preordered type `α` with `s` bounded below, then `s ∩ t` is also bounded below.
`isLUB_Ioo` theorem isLUB_Ioo : ∀ {γ : Type w} [inst : SemilatticeInf γ] [inst_1 : DenselyOrdered γ] {a b : γ}, a < b → IsLUB (Set.Ioo a b) b := by sorry The theorem `isLUB_Ioo` states that for any type `γ` that is a semilattice under the infimum operation and is densely ordered, and for any two elements `a` and `b` of `γ` such that `a` is less than `b`, `b` is a least upper bound of the open interval `(a, b)`. In other words, no element in the open interval `(a, b)` is greater than `b`, and any element greater than or equal to `b` is not in the interval `(a, b)`. More concisely: For any semilattice `γ` with dense order and any `a < b` in `γ`, `b` is the least upper bound of the open interval `(a, b)`.
`bddBelow_union` theorem bddBelow_union : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] {s t : Set α}, BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t In the context of a preorder (a set equipped with a reflexive and transitive binary relation) that is codirected (for any two elements there exists a common lower bound), the theorem `bddBelow_union` states that for any two sets `s` and `t` of type `α`, the union of these two sets is bounded below if and only if both `s` and `t` are themselves bounded below. In mathematical terms, there exists a lower bound for the union of two sets `s ∪ t` if and only if there exist lower bounds for both sets `s` and `t` individually. More concisely: In a codirected preorder, two sets have a lower bound for their union if and only if each set has a lower bound individually.
`MonotoneOn.map_bddBelow` theorem MonotoneOn.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, MonotoneOn f t → s ⊆ t → (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s) This theorem states that if we have a function `f` that is monotone on a set `t`, and we have a subset `s` of `t` which has a lower bound within `t`, then the image of `s` under `f` is also bounded below. In other words, the application of a monotone function preserves the property of having a lower bound. In mathematical terms, if for every `a` and `b` in `t`, `a ≤ b` implies `f(a) ≤ f(b)`, and there exists an element in `t` which is lesser than or equal to every element in `s`, then there exists an element which is lesser than or equal to every element in the set formed by applying `f` to each element in `s`. More concisely: If a monotonic function maps a set with a lower bound to another set, then the image of that set has a lower bound as well.
`IsGLB.union` theorem IsGLB.union : ∀ {γ : Type w} [inst : SemilatticeInf γ] {a₁ a₂ : γ} {s t : Set γ}, IsGLB s a₁ → IsGLB t a₂ → IsGLB (s ∪ t) (a₁ ⊓ a₂) The theorem `IsGLB.union` states that for any type `γ` that forms a semilattice under the operation "infimum" (denoted by `⊓`), if `a₁` is the greatest lower bound of a set `s` and `a₂` is the greatest lower bound of another set `t`, then the infimum of `a₁` and `a₂` is the greatest lower bound of the union of `s` and `t`. In other words, for any two sets `s` and `t`, their greatest lower bounds' infimum is the greatest lower bound of the union of `s` and `t`. More concisely: For any semilattices `γ` and sets `s` and `t` with greatest lower bounds `a₁` and `a₂` respectively, the infimum of `a₁` and `a₂` is equal to the greatest lower bound of `s ∪ t`.
`Mathlib.Order.Bounds.Basic._auxLemma.32` theorem Mathlib.Order.Bounds.Basic._auxLemma.32 : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] (s : Set α), BddAbove s = True This theorem states that for any given type `α` which has a preorder and is an ordered top, every set `s` of type `α` is bounded above. In other words, given any set `s` in this context, there exists an upper bound for this set. This is demonstrated by the fact that `BddAbove s` is always True. More concisely: Every non-empty set in an ordered type with a greatest element is bounded above.
`Set.Nonempty.bddBelow_upperBounds` theorem Set.Nonempty.bddBelow_upperBounds : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, s.Nonempty → BddBelow (upperBounds s) The theorem `Set.Nonempty.bddBelow_upperBounds` states that for any type `α` with a preorder structure and for any nonempty set `s` of type `α`, the set of upper bounds of `s` has a lower bound. In simple terms, this theorem asserts that if we have a nonempty set, the collection of all elements which are greater than or equal to every element in the set, has at least one element that is smaller than or equal to all others in this collection. More concisely: If `α` is a type with a preorder structure and `s ≠∅` is a set of `α`, then the set of upper bounds of `s` has a least element.
`MonotoneOn.map_bddAbove` theorem MonotoneOn.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, MonotoneOn f t → s ⊆ t → (upperBounds s ∩ t).Nonempty → BddAbove (f '' s) The theorem `MonotoneOn.map_bddAbove` states that for any types `α` and `β`, and any preorders defined on them, given a function `f` from `α` to `β`, and two sets `s` and `t` of type `α`, if `f` is monotone on `t`, `s` is a subset of `t`, and `s` has at least one upper bound in `t`, then the image of `s` under `f` is bounded above. In other words, if we apply a monotone function to every element of a set that has an upper bound, the resulting set also has an upper bound. This captures a property of monotone functions, which preserve the order and bounds of sets. More concisely: If `f` is a monotone function and `s ⊆ t` are sets with `s` having an upper bound in `t`, then `f``(s)` has an upper bound.
`upperBounds_singleton` theorem upperBounds_singleton : ∀ {α : Type u} [inst : Preorder α] {a : α}, upperBounds {a} = Set.Ici a This theorem states that for any type `α` equipped with a preorder and any element `a` of type `α`, the set of upper bounds of the singleton set containing just `a` is equivalent to the set of all elements in `α` that are greater than or equal to `a`. In other words, the upper bounds of a singleton set `{a}` is the set of all elements `x` such that `a` is less than or equal to `x`. More concisely: The set of upper bounds for a singleton set {a} in a preordered type equals the set of elements greater than or equal to a.
`IsGreatest.isLUB` theorem IsGreatest.isLUB : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → IsLUB s a := by sorry The theorem `IsGreatest.isLUB` states that for all types `α` with a preorder structure, for any set `s` of type `α` and any element `a` of type `α`, if `a` is the greatest element of the set `s`, then `a` is also the least upper bound of the set `s`. In other words, if an element is the greatest element in a set (with respect to a given preorder), then it also serves as the least upper bound for that set. More concisely: If `α` is a type with a preorder structure, and `a` is the greatest element of a set `s` in `α`, then `a` is the least upper bound of `s`.
`Antitone.map_bddBelow` theorem Antitone.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Antitone f → ∀ {s : Set α}, BddBelow s → BddAbove (f '' s) This theorem states that if you have an antitone function (a function where an increase in the input leads to a decrease in the output), and you apply this function to a set that is bounded below (meaning there exists a value which is less than or equal to all elements of the set), then the image of this set under the function is bounded above. In other words, there exists a value that is greater than or equal to all elements of the image set. In mathematical language, given an antitone function $f: \alpha \to \beta$ and a set $s$ in $\alpha$ such that $s$ is bounded below, then the image of $s$ under $f$, denoted by $f(s)$, is bounded above. More concisely: If $f: \alpha \to \beta$ is an antitone function and $s \subseteq \alpha$ is bounded below, then $f(s)$ has a supremum in $\beta$.
`not_bddBelow_iff'` theorem not_bddBelow_iff' : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, ¬x ≤ y In natural language, the theorem `not_bddBelow_iff'` can be described as follows: A set `s` of elements of some type `α` (where `α` has a preorder structure) is not bounded below if and only if for every element `x` of type `α`, there exists an element `y` in the set `s` such that `x` is not less than or equal to `y`. In other words, no matter what `x` you choose, you can always find a `y` in `s` that is strictly greater than `x`. This theorem applies in the general case of preorders, and uses negation (`¬x ≤ y`) to express "not less than or equal to". A different version applies for linear orders. More concisely: A preorder `s` subset of type `α` has no lowest element if and only if for every `x` in `α`, there exists `y` in `s` such that `x` is not less than or equal to `y`.
`isLUB_singleton` theorem isLUB_singleton : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsLUB {a} a The theorem `isLUB_singleton` asserts that for any type `α` equipped with a preorder, and any element `a` of type `α`, `a` is a least upper bound of the singleton set `{a}`. In other words, `a` is the smallest element that is greater than or equal to every element in the set `{a}`, which in this case, only contains `a` itself. More concisely: For any preordered type `α` and element `a` in `α`, `a` is the least upper bound of the singleton set `{a}`.
`isGreatest_singleton` theorem isGreatest_singleton : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsGreatest {a} a This theorem states that for any preorder set `α` and any element `a` from that set, `a` is the greatest element of the singleton set `{a}`. In other words, in the context of a partial order, `a` is the unique greatest element of its own singleton set. This makes sense because a singleton set contains only one element, so that element is trivially the greatest (and least) element within that set. More concisely: For any preorder set `α` and its element `a`, `a` is the greatest element of the singleton set `{a}`. In a partial order context, `a` is the unique greatest element of its own singleton set.
`IsGreatest.union` theorem IsGreatest.union : ∀ {γ : Type w} [inst : LinearOrder γ] {a b : γ} {s t : Set γ}, IsGreatest s a → IsGreatest t b → IsGreatest (s ∪ t) (max a b) The theorem `IsGreatest.union` states that for any type `γ` that has a linear order, given two sets `s` and `t` of this type and two elements `a` and `b` such that `a` is the greatest element in `s` and `b` is the greatest element in `t`, then the greatest element of the union of `s` and `t` is the maximum of `a` and `b`. Here, 'greatest' means that the element is in the set and no other element in the set is greater than it, following the `IsGreatest` definition; 'maximum' refers to the larger of the two elements `a` and `b` according to the linear order on `γ`. More concisely: Given two sets `s` and `t` of a linearly ordered type `γ`, and elements `a` in `s` and `b` in `t` as their greatest elements, then `max a b` is the greatest element in `s ∪ t`.
`Antitone.map_isGreatest` theorem Antitone.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Antitone f → ∀ {a : α} {s : Set α}, IsGreatest s a → IsLeast (f '' s) (f a) The theorem `Antitone.map_isGreatest` states that for any antitone function `f` (a function where if `a ≤ b` then `f(b) ≤ f(a)`) and any set `s` of elements of some type `α`, if `a` is the greatest element in `s`, then `f(a)` is the least element in the image set `f(s)`. Here, "greatest" and "least" elements are defined with respect to a preorder, a binary relation that is reflexive and transitive. This means that, under a preorder, if `a` is the greatest element of a set, then it is greater than or equal to every other element in the set, and if `f(a)` is the least element of its image set `f(s)`, then it is less than or equal to every other element in that set. More concisely: If `f` is an antitone function and `a` is the greatest element in a set `s`, then `f(a)` is the least element in the image `f(s)`.
`IsLeast.bddBelow` theorem IsLeast.bddBelow : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → BddBelow s The theorem `IsLeast.bddBelow` states that for any set `s` of a certain type `α` with the structure of a preorder, if there exists an element `a` which is the least element in the set `s` (i.e., `a` both belongs to `s` and is a lower bound of `s`), then the set `s` is bounded below. In other words, if a set has a least element, then there exists a lower bound for the set. More concisely: If a preorder set `s` of type `α` has a least element, then `s` is bounded below.
`upperBounds_insert` theorem upperBounds_insert : ∀ {α : Type u} [inst : Preorder α] (a : α) (s : Set α), upperBounds (insert a s) = Set.Ici a ∩ upperBounds s := by sorry The theorem `upperBounds_insert` states that for any type `α` that has a pre-order relation (a relation that is reflexive and transitive), for any element `a` of type `α` and any set `s` of elements of type `α`, the set of upper bounds of the set obtained by inserting `a` into `s` is equal to the intersection of the set of all elements that are greater than or equal to `a` and the set of upper bounds of `s`. In other words, an element is an upper bound of the inserted set if and only if it is an upper bound of the original set `s` and is also greater than or equal to `a`. More concisely: For any pre-order relation on type `α`, the upper bounds of an element `a` inserted into a set `s` equal the intersection of the upper bounds of `s` and elements greater than or equal to `a`.
`BddAbove.union` theorem BddAbove.union : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] {s t : Set α}, BddAbove s → BddAbove t → BddAbove (s ∪ t) In the context of a preordered type `α`, where any two elements of `α` have an upper bound, the theorem `BddAbove.union` states that if two sets, `s` and `t`, are each bounded above, then their union is also bounded above. In other words, if there exists an upper bound for each of the sets `s` and `t`, there also exists an upper bound for the set `s ∪ t`. More concisely: If `α` is a preordered type with the property that any two elements have an upper bound, then the union of two bounded sets `s` and `t` is also bounded above.
`BddAbove.image2` theorem BddAbove.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Monotone (f a)) → BddAbove s → BddAbove t → BddAbove (Set.image2 f s t) This theorem states that for any types `α`, `β`, `γ` with preorders, a binary function `f : α → β → γ`, and sets `s` of type `α` and `t` of type `β`, if for every element `b` of type `β`, the function obtained by swapping the arguments of `f` and then fixing `b` is monotone, and for every element `a` of type `α`, the function obtained from `f` by fixing `a` is monotone, then if `s` and `t` are both bounded above, the image of the Cartesian product of `s` and `t` under `f` is also bounded above. In other words, if `f` is monotone in each argument and both `s` and `t` have upper bounds, then the set of all values that `f` can take on pairs `(a, b)` where `a` is from `s` and `b` is from `t`, also has an upper bound. More concisely: If `f : α → β → γ` is a monotonic function between preordered types `α`, `β`, and `γ`, and sets `s` of type `α` and `t` of type `β` have upper bounds, then the image of their Cartesian product under `f` is also bounded above.
`mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds` theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Antitone (f a)) → a ∈ lowerBounds s → b ∈ upperBounds t → f a b ∈ lowerBounds (Set.image2 f s t) This theorem states that for any types `α`, `β`, and `γ`, with preorder relations defined on them, and any sets `s` of type `α` and `t` of type `β`, if you have a binary function `f : α → β → γ` such that for every `β`, swapping the arguments of `f` gives a monotone function, and for every `α`, `f` is an antitone function, then if `a` is a lower bound of `s` and `b` is an upper bound of `t`, the result of the function `f a b` is a lower bound of the image of the function `f` applied to `s` and `t`. In simpler terms, if `a` is a lower bound for a set and `b` is an upper bound for another set, and `f` is a function that increases as one argument increases and decreases as the other argument increases, the value `f a b` will be a lower bound for all possible values of `f` over the two sets. More concisely: If `α` and `β` are types with preorders, `s` is a set of type `α`, `t` is a set of type `β`, `f : α → β → γ` is a function such that `f` is monotone in the second argument for every fixed first argument and antitone in the first argument for every fixed second argument, and `a` is a lower bound of `s` and `b` is an upper bound of `t`, then `f a b` is a lower bound of the image of `f` on `s × t`.
`IsLUB.union` theorem IsLUB.union : ∀ {γ : Type w} [inst : SemilatticeSup γ] {a b : γ} {s t : Set γ}, IsLUB s a → IsLUB t b → IsLUB (s ∪ t) (a ⊔ b) This theorem states that in a semilattice (a structure with a partial order where every two elements have a least upper bound), if 'a' is the least upper bound of a set 's' and 'b' is the least upper bound of another set 't', then the join of 'a' and 'b' (denoted as 'a ⊔ b') is the least upper bound of the union of 's' and 't'. In other words, the least upper bound of the union of two sets is the join of the least upper bounds of the individual sets. More concisely: In a semilattice, the least upper bound of the union of two sets is the join of their least upper bounds.
`isGLB_Ioc` theorem isGLB_Ioc : ∀ {γ : Type w} [inst : SemilatticeSup γ] [inst_1 : DenselyOrdered γ] {a b : γ}, a < b → IsGLB (Set.Ioc a b) a := by sorry The theorem `isGLB_Ioc` states that for any type `γ` which forms a semilattice with a supremum operation and is densely ordered, and for any two elements `a` and `b` of this type such that `a` is less than `b`, `a` is the greatest lower bound of the set formed by the half-open interval from `a` to `b` (where `a` is not included in the interval but `b` is). More concisely: For any semilattice `γ` with supremum and dense order, if `a` is a lower bound of the half-open interval `[a, b)` in `γ`, then `a` is the greatest lower bound of that interval.
`lt_isLUB_iff` theorem lt_isLUB_iff : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α} {a b : α}, IsLUB s a → (b < a ↔ ∃ c ∈ s, b < c) This theorem states that for any type `α` with a linear order, and any set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `a` is a least upper bound of `s`, then `b` is less than `a` if and only if there exists an element `c` in `s` such that `b` is less than `c`. In other words, an element `b` is less than the least upper bound `a` of a set `s` precisely when there is an element `c` in the set `s` that `b` fails to exceed. More concisely: For any linear order `α`, set `s` of type `α`, and elements `a` and `b` of type `α`, if `a` is the least upper bound of `s`, then `b` is strictly less than `a` if and only if there exists an element `c` in `s` such that `b` is strictly less than `c`.
`bddAbove_union` theorem bddAbove_union : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≤ x_1] {s t : Set α}, BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t The theorem `bddAbove_union` states that for a given type `α` equipped with a preorder relation and a directed order relation (meaning that for any two elements, there is a third element that is greater than or equal to both), and for any two sets `s` and `t` of this type, the union of `s` and `t` is bounded above if and only if both `s` and `t` are individually bounded above. In other words, a set union has an upper bound in this ordered type if and only if both of the original sets have an upper bound. More concisely: For sets `s` and `t` in a type `α` equipped with a preorder and a directed order relation, `s ∪ t` has an upper bound if and only if both `s` and `t` have upper bounds.
`MonotoneOn.map_isGreatest` theorem MonotoneOn.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α}, MonotoneOn f t → ∀ {a : α}, IsGreatest t a → IsGreatest (f '' t) (f a) The theorem `MonotoneOn.map_isGreatest` states that if a function `f` from type `α` to type `β` is monotone on a set `t` of type `α`, then for any greatest element `a` of the set `t`, the image of `a` under `f`, denoted as `f(a)`, is the greatest element of the image set `f '' t`. This means that a monotone map preserves the ordering of elements when mapping a greatest element of a set to the greatest element of its image set. Both `α` and `β` are types equipped with a preorder (i.e., a relation that is reflexive and transitive). More concisely: If `f` is a monotone function from a preordered set `(α, ≤)` to another preordered set `(β, ≤)` and `a` is the greatest element of `t ⊆ α`, then `f(a)` is the greatest element of `f(t)`.
`mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds` theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β}, (∀ (b : β), Monotone (Function.swap f b)) → (∀ (a : α), Antitone (f a)) → a ∈ upperBounds s → b ∈ lowerBounds t → f a b ∈ upperBounds (Set.image2 f s t) This theorem states that for any types `α`, `β`, and `γ` with preorder relations, given a binary function `f` from `α` to `β` to `γ`, sets `s` of `α` and `t` of `β`, and elements `a` of `α` and `b` of `β`, if every function obtained by fixing `b` in `f` is monotone and every function obtained by fixing `a` in `f` is antitone, and if `a` is an upper bound of `s` and `b` is a lower bound of `t`, then `f(a,b)` is an upper bound of the image of `s` and `t` under `f`. In simpler terms, if `f` increases with `a` for every fixed `b` and decreases with `b` for every fixed `a`, and `a` and `b` are upper and lower bounds of their respective sets, then `f(a,b)` is an upper bound of all values of `f` when `f` is applied to elements from `s` and `t`. More concisely: If functions `f: α → β → γ`, `s ⊆ α`, `t ⊆ β`, `a ∈ s` is an upper bound of `s`, `b ∈ t` is a lower bound of `t`, `f` is increasing in `a` for every `b` and decreasing in `b` for every `a`, then `f(a,b)` is an upper bound of `{f(x,y) \| x ∈ s, y ∈ t}`.
`IsLUB.insert` theorem IsLUB.insert : ∀ {γ : Type w} [inst : SemilatticeSup γ] (a : γ) {b : γ} {s : Set γ}, IsLUB s b → IsLUB (insert a s) (a ⊔ b) := by sorry This theorem, `IsLUB.insert`, states that for any type `γ` that has a semilattice structure, given any two elements `a` and `b` of this type and a set `s` of elements of the same type, if `b` is a least upper bound of the set `s`, then the least upper bound of the set obtained by inserting `a` into `s` is the supremum of `a` and `b`. The supremum (`⊔`) is the smallest element that is greater than or equal to both `a` and `b` in the semilattice. More concisely: For any semilattice type `γ` and elements `a`, `b` in `γ`, if `b` is the least upper bound of a set `s` in `γ`, then `a⊔b` is the least upper bound of `s∪{a}`.
`lub_Iio_le` theorem lub_Iio_le : ∀ {α : Type u} [inst : Preorder α] {b : α} (a : α), IsLUB (Set.Iio a) b → b ≤ a This theorem states that for any type `α` that has a preorder structure, and for any elements `b` and `a` of that type, if `b` is a least upper bound (also known as supremum) of the set of all elements less than `a` (i.e., the left-infinite right-open interval up to `a`), then `b` is less than or equal to `a`. In simple terms, the smallest number that's larger than all numbers less than `a` is always less than or equal to `a` itself. More concisely: For any type `α` with a preorder structure and any element `a` of `α`, if `b` is the least upper bound of the elements less than `a`, then `b` is less than or equal to `a`.
`not_bddBelow_iff` theorem not_bddBelow_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, y < x The theorem `not_bddBelow_iff` describes a condition for a set `s` of a certain type `α` under a linear order to not be bounded below. The theorem states that a set `s` is not bounded below if and only if for every element `x` of type `α`, there exists an element `y` in the set `s` such that `y` is less than `x`. This theorem provides a characterization for sets that lack a lower bound in the context of linear orders. More concisely: A set of type `α` under a linear order is not bounded below if and only if for every `x` in `α`, there exists `y` in the set such that `y` is strictly less than `x`.
`IsLUB.exists_between` theorem IsLUB.exists_between : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α} {a b : α}, IsLUB s a → b < a → ∃ c ∈ s, b < c ∧ c ≤ a The theorem `IsLUB.exists_between` states that for any type `α` under a linear order, given a set `s` of type `α` and two elements `a` and `b` of type `α`, if `a` is a least upper bound of the set `s` and `b` is strictly less than `a`, then there exists an element `c` in the set `s` such that `b` is strictly less than `c` and `c` is less than or equal to `a`. In other words, when `a` is the least upper bound of `s` and `b` is less than `a`, there is always an element `c` from `s` that lies between `b` and `a`. More concisely: If `a` is the least upper bound of a set `s` in a linear order and `b` is strictly less than `a`, then there exists an element `c` in `s` with `b` strictly less than `c` and `c` less than or equal to `a`.
`IsLUB.upperBounds_eq` theorem IsLUB.upperBounds_eq : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → upperBounds s = Set.Ici a This theorem states that for any set `s` of a type `α` under a Preorder relation, if a number `a` is a least upper bound of `s`, then the set of all upper bounds of `s` is equivalent to the set of all numbers greater than or equal to `a`. In mathematical terms, if `a` is a least upper bound (LUB) of a set `s`, then the set of upper bounds of `s` is the same as the interval `[a, +∞)`. More concisely: If `a` is the least upper bound of a set `s` under a preorder relation, then the set of upper bounds of `s` is equal to the set of numbers greater than or equal to `a`.
`IsLUB.dual` theorem IsLUB.dual : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a) This theorem states that for any given type `α` with a preorder relationship and any set `s` of elements of this type, if `a` is a least upper bound (LUB) of this set `s`, then `a` is also the greatest lower bound (GLB) of the set `s` under the order dual transformation. The order dual transforms each element of the set `s` to its dual order, effectively reversing the order of the elements. The theorem thus asserts that the LUB in the original order becomes the GLB in the reversed order. More concisely: For any preordered type `α` and set `s` of elements, if `a` is the least upper bound of `s`, then `a` is also the greatest lower bound of `s` in the order dual.
`bddBelow_insert` theorem bddBelow_insert : ∀ {α : Type u} [inst : Preorder α] [inst_1 : IsDirected α fun x x_1 => x ≥ x_1] {s : Set α} {a : α}, BddBelow (insert a s) ↔ BddBelow s The theorem `bddBelow_insert` states that for any type `α` that has a preorder and is directed (meaning for any two elements there exists a common upper bound), any set `s` of this type, and any element `a` of the same type, inserting `a` into `s` preserves the property of being bounded below. In other words, if the set `s` has a lower bound, then the set obtained by adding `a` to `s` also has a lower bound, and vice versa. More concisely: For any directed type `α` with a preorder, if a set `s` of `α` has a lower bound, then the set `s.insert a` also has a lower bound, where `a` is an element of `α`.
`IsLeast.union` theorem IsLeast.union : ∀ {γ : Type w} [inst : LinearOrder γ] {a b : γ} {s t : Set γ}, IsLeast s a → IsLeast t b → IsLeast (s ∪ t) (min a b) The theorem `IsLeast.union` states that for any type `γ` which has a linear order, given two elements `a` and `b` of `γ` and two sets `s` and `t` of `γ`, if `a` is the least element of set `s` and `b` is the least element of set `t`, then the minimum of `a` and `b` is the least element of the union of sets `s` and `t`. In essence, it's asserting that the least element of the union of two sets is the smaller of the least elements of each set. More concisely: If `γ` is a linedarly ordered type, `a` is the least element of set `s`, `b` is the least element of set `t`, then `min a b` is the least element of `s ∪ t`.
`lowerBounds_mono_set` theorem lowerBounds_mono_set : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → lowerBounds t ⊆ lowerBounds s The theorem `lowerBounds_mono_set` states that for any type `α` with a preorder (`≤`), and any two sets `s` and `t` of type `α`, if `s` is a subset of `t`, then the set of lower bounds of `t` is a subset of the set of lower bounds of `s`. This means that any lower bound of the larger set `t` is also a lower bound of the smaller set `s`. In other words, if every element of `s` is also in `t`, then every lower bound for `t` is also a lower bound for `s`. More concisely: If `s` is a subset of `t` in a preordered type `α`, then the set of lower bounds of `t` includes the set of lower bounds of `s`.
`upperBounds_union` theorem upperBounds_union : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t This theorem states that for any two sets `s` and `t` of some type `α` which has a preorder (a binary relation that is reflexive and transitive), the set of upper bounds of the union of `s` and `t` is equal to the intersection of the set of upper bounds of `s` and the set of upper bounds of `t`. In more mathematical terms, this theorem is saying that $\operatorname{upperBounds}(s \cup t) = \operatorname{upperBounds}(s) \cap \operatorname{upperBounds}(t)$. An upper bound of a set is an element that is greater than or equal to every element in the set. More concisely: For sets `s` and `t` in type `α` with a preorder, the set of upper bounds of their union equals the intersection of the upper bounds of `s` and `t`. In mathematical notation, $\operatorname{upperBounds}(s \cup t) = \operatorname{upperBounds}(s) \cap \operatorname{upperBounds}(t)$.
`bddAbove_Icc` theorem bddAbove_Icc : ∀ {α : Type u} [inst : Preorder α] {a b : α}, BddAbove (Set.Icc a b) This theorem states that for any type `α` that has an order structure (preorder), and for any two elements `a` and `b` of this type, the closed interval `Set.Icc a b` (which includes all elements `x` such that `a ≤ x` and `x ≤ b`) is bounded above. This means there exists an element which is greater than or equal to every element in the closed interval `Set.Icc a b`. More concisely: For any type `α` with an order structure and any `a, b ∈ α` with `a ≤ b`, the closed interval `[a, b] = {x \| a ≤ x ≤ b}` has a supreme element.
`AntitoneOn.map_bddBelow` theorem AntitoneOn.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, AntitoneOn f t → s ⊆ t → (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s) The theorem `AntitoneOn.map_bddBelow` states that for any types `α` and `β` that have preorder structures, and any function `f` from `α` to `β`, if `f` is antitone (meaning it reverses the order) on a set `t`, and there is a set `s` which is a subset of `t` that has a nonempty intersection with its lower bounds, then the image of `s` under `f` is bounded above. In other words, if we have a function that reverses order on a certain set and another set that is bounded below, the image of the second set under the function will have an upper bound. More concisely: If `f: α → β` is an antitone function between preordered types `α` and `β`, and `s ⊆ t` has a nonempty intersection with the lower bounds of `t`, then the image `f''s` is bounded above in `β`.

LeanAide GPT-4 documentation

Module: Mathlib.Order.Bounds.Basic

IsLUB.bddAbove

theorem IsLUB.bddAbove : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a → BddAbove s

Monotone.map_bddAbove

theorem Monotone.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, BddAbove s → BddAbove (f '' s)

isLUB_pair

theorem isLUB_pair : ∀ {γ : Type w} [inst : SemilatticeSup γ] {a b : γ}, IsLUB {a, b} (a ⊔ b)

IsLUB.of_subset_of_superset

theorem IsLUB.of_subset_of_superset : ∀ {α : Type u} [inst : Preorder α] {a : α} {s t p : Set α}, IsLUB s a → IsLUB p a → s ⊆ t → t ⊆ p → IsLUB t a := by sorry

BddBelow.inter_of_right

theorem BddBelow.inter_of_right : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddBelow t → BddBelow (s ∩ t) := by sorry

upperBounds_empty

theorem upperBounds_empty : ∀ {α : Type u} [inst : Preorder α], upperBounds ∅ = Set.univ

isGreatest_Iic

theorem isGreatest_Iic : ∀ {α : Type u} [inst : Preorder α] {a : α}, IsGreatest (Set.Iic a) a

BddAbove.mono

theorem BddAbove.mono : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddAbove t → BddAbove s

mem_upperBounds_image2

IsGreatest.unique

theorem IsGreatest.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGreatest s a → IsGreatest s b → a = b

upperBounds_mono_set

theorem upperBounds_mono_set : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → upperBounds t ⊆ upperBounds s

not_bddAbove_iff'

theorem not_bddAbove_iff' : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x

Monotone.map_isLeast

theorem Monotone.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, IsLeast s a → IsLeast (f '' s) (f a)

Monotone.map_isGreatest

theorem Monotone.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, IsGreatest s a → IsGreatest (f '' s) (f a)

IsGLB.of_subset_of_superset

theorem IsGLB.of_subset_of_superset : ∀ {α : Type u} [inst : Preorder α] {a : α} {s t p : Set α}, IsGLB s a → IsGLB p a → s ⊆ t → t ⊆ p → IsGLB t a := by sorry

Set.Nonempty.bddAbove_lowerBounds

theorem Set.Nonempty.bddAbove_lowerBounds : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, s.Nonempty → BddAbove (lowerBounds s)

lowerBounds_empty

theorem lowerBounds_empty : ∀ {α : Type u} [inst : Preorder α], lowerBounds ∅ = Set.univ

isGLB_Icc

theorem isGLB_Icc : ∀ {α : Type u} [inst : Preorder α] {a b : α}, a ≤ b → IsGLB (Set.Icc a b) a

IsLeast.isGLB

theorem IsLeast.isGLB : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → IsGLB s a

mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds

Monotone.mem_upperBounds_image

theorem Monotone.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, a ∈ upperBounds s → f a ∈ upperBounds (f '' s)

mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds

AntitoneOn.map_isLeast

theorem AntitoneOn.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α}, AntitoneOn f t → ∀ {a : α}, IsLeast t a → IsGreatest (f '' t) (f a)

Monotone.mem_lowerBounds_image

theorem Monotone.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {a : α} {s : Set α}, a ∈ lowerBounds s → f a ∈ lowerBounds (f '' s)

not_bddAbove_iff

theorem not_bddAbove_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y

isGreatest_univ

theorem isGreatest_univ : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α], IsGreatest Set.univ ⊤

IsGLB.dual

theorem IsGLB.dual : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)

BddBelow.mono

theorem BddBelow.mono : ∀ {α : Type u} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → BddBelow t → BddBelow s

BddAbove.inter_of_right

theorem BddAbove.inter_of_right : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddAbove t → BddAbove (s ∩ t) := by sorry

IsGLB.exists_between

theorem IsGLB.exists_between : ∀ {α : Type u} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → a < b → ∃ c ∈ s, a ≤ c ∧ c < b

OrderBot.bddBelow

theorem OrderBot.bddBelow : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] (s : Set α), BddBelow s

bddAbove_Iio

theorem bddAbove_Iio : ∀ {α : Type u} [inst : Preorder α] {a : α}, BddAbove (Set.Iio a)

Monotone.map_bddBelow

theorem Monotone.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, BddBelow s → BddBelow (f '' s)

AntitoneOn.map_bddAbove

theorem AntitoneOn.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α}, AntitoneOn f t → s ⊆ t → (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)

BddAbove.inter_of_left

theorem BddAbove.inter_of_left : ∀ {α : Type u} [inst : Preorder α] {s t : Set α}, BddAbove s → BddAbove (s ∩ t) := by sorry

IsGLB.lowerBounds_eq

theorem IsGLB.lowerBounds_eq : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a : α}, IsGLB s a → lowerBounds s = Set.Iic a

IsGLB.unique

theorem IsGLB.unique : ∀ {α : Type u} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGLB s a → IsGLB s b → a = b := by sorry

isLUB_le_iff

theorem isLUB_le_iff : ∀ {α : Type u} [inst : Preorder α] {s : Set α} {a b : α}, IsLUB s a → (a ≤ b ↔ b ∈ upperBounds s)

Monotone.image_upperBounds_subset_upperBounds_image

theorem Monotone.image_upperBounds_subset_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β}, Monotone f → ∀ {s : Set α}, f '' upperBounds s ⊆ upperBounds (f '' s)

isLUB_Ico

theorem isLUB_Ico : ∀ {γ : Type w} [inst : SemilatticeInf γ] [inst_1 : DenselyOrdered γ] {a b : γ}, a < b → IsLUB (Set.Ico a b) b := by sorry

bddAbove_insert

`IsLUB.bddAbove`

`Monotone.map_bddAbove`

`isLUB_pair`

`IsLUB.of_subset_of_superset`

`BddBelow.inter_of_right`

`upperBounds_empty`

`isGreatest_Iic`

`BddAbove.mono`

`mem_upperBounds_image2`

`IsGreatest.unique`

`upperBounds_mono_set`

`not_bddAbove_iff'`

`Monotone.map_isLeast`

`Monotone.map_isGreatest`

`IsGLB.of_subset_of_superset`

`Set.Nonempty.bddAbove_lowerBounds`

`lowerBounds_empty`

`isGLB_Icc`

`IsLeast.isGLB`

`mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds`

`Monotone.mem_upperBounds_image`

`mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds`

`AntitoneOn.map_isLeast`

`Monotone.mem_lowerBounds_image`

`not_bddAbove_iff`

`isGreatest_univ`

`IsGLB.dual`

`BddBelow.mono`

`BddAbove.inter_of_right`

`IsGLB.exists_between`

`OrderBot.bddBelow`

`bddAbove_Iio`

`Monotone.map_bddBelow`

`AntitoneOn.map_bddAbove`

`BddAbove.inter_of_left`

`IsGLB.lowerBounds_eq`

`IsGLB.unique`

`isLUB_le_iff`

`Monotone.image_upperBounds_subset_upperBounds_image`

`isLUB_Ico`

`bddAbove_insert`

`mem_lowerBounds_image2`

`mem_upperBounds_image2_of_mem_lowerBounds`

`MonotoneOn.mem_lowerBounds_image`

`OrderTop.bddAbove`

`MonotoneOn.mem_upperBounds_image`

`isLeast_Ici`

`isGLB_Ioo`

`le_isGLB_iff`

`mem_upperBounds`

`IsGLB.of_image`

`isGLB_singleton`

`bddAbove_range_prod`

`isLeast_singleton`

`IsLUB.unique`

`Antitone.map_isLeast`

`upperBounds_mono_mem`

`IsGLB.bddBelow`

`AntitoneOn.map_isGreatest`

`Mathlib.Order.Bounds.Basic._auxLemma.21`

`MonotoneOn.map_isLeast`

`BddBelow.union`

`BddBelow.image2`

`mem_lowerBounds`

`IsGreatest.bddAbove`

`isGLB_lt_iff`

`mem_lowerBounds_image2_of_mem_upperBounds`

`bddBelow_Icc`

`Antitone.map_bddAbove`

`IsLeast.unique`

`BddBelow.inter_of_left`

`isLUB_Ioo`

`bddBelow_union`

`MonotoneOn.map_bddBelow`