IsUpperSet.ordConnected
theorem IsUpperSet.ordConnected : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → s.OrdConnected := by
sorry
The theorem `IsUpperSet.ordConnected` states that for all types `α` with a preorder structure, if a set `s` of type `α` is an upper set, then `s` is also order connected. In other words, if a set `s` has the property that any element greater than one of its members is also a member of the set (`IsUpperSet`), then for any two elements in this set, every element that lies between the two is also in the set (`Set.OrdConnected`). This is a property inherent to upper sets in a preordered set.
More concisely: If `s` is an upper set in a preordered type `α`, then `s` is order connected, i.e., for all `a` and `b` in `s`, every element `x` with `a < x < b` is also in `s`.
|
UpperSet.coe_iInf
theorem UpperSet.coe_iInf :
∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), ↑(⨅ i, f i) = ⋃ i, ↑(f i)
This theorem, `UpperSet.coe_iInf`, states that for any type `α` and any sort `ι`, given a certain less-or-equals relationship on `α`, and a function `f` from `ι` to the set of upper sets of `α`, the intersection over all `ι` of the co-domain of `f` is equivalent to the union over all `ι` of the individual co-domains of `f`. In other words, in this context, intersecting all `f i` and then taking the upper set is the same as taking the upper set of each `f i` and then uniting them all.
More concisely: For any type `α` and sort `ι`, if `f : ι → upperSets α` satisfies `∀ i, ∀ x ∈ i, x ≤ x' → f i x ∩ f i x' = f i x ∪ f i x'`, then `⋂ i, f i = ⋃ i, f i`.
|
UpperSet.coe_iSup
theorem UpperSet.coe_iSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), ↑(⨆ i, f i) = ⋂ i, ↑(f i)
This theorem states that for any type `α` and any type `ι`, given a function `f` from `ι` to the upper sets of `α`, the supremum of the image of `f` (`⨆ i, f i`) is equal to the intersection of the images of `f` (`⋂ i, ↑(f i)`). Here, `⨆` denotes the supremum, `⋂` denotes the intersection, and `↑` denotes the coe function which converts `UpperSet α` to `Set α`. This is in the context of `α` being a type with a less than or equal to relation (`LE α`).
More concisely: For any type `α` with a less than or equal to relation and any function `f` from type `ι` to the upper sets of `α`, the supremum of `f` is equal to the intersection of the images of `f` taken pointwise and converted to sets.
|
LowerSet.coe_iInf₂
theorem LowerSet.coe_iInf₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
This theorem states that for any type `α` equipped with a less than or equal to relation (i.e., a pre-order), and for any indexed collection of sorts `ι` and `κ`, given a function `f` that takes an index `i` from `ι` and an index `j` from `κ i` and produces a lower set of `α`, the infimum (greatest lower bound) over all `i` and `j` of the elements of `f` is equal to the intersection over all `i` and `j` of the elements of `f`. In simple terms, it says that the greatest lower bound of a collection of lower sets can be obtained by intersecting all of those lower sets.
More concisely: For any pre-order (α, ≤), given an indexed family of subsets {F i : ι → α : i ∈ ι} where each F i is a lower set, the infimum of the F i is equal to the intersection of the F i.
|
isLowerSet_sUnion
theorem isLowerSet_sUnion :
∀ {α : Type u_1} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsLowerSet s) → IsLowerSet S.sUnion
The theorem `isLowerSet_sUnion` states that for any type `α` that has a less than or equal to relation, and any collection `S` of sets of type `α`, if every set in `S` is a lower set, then the union over all sets in `S` is also a lower set. In other words, if every set in `S` has the property that any element less than or equal to one of its members is also a member of the set, then the same property holds for the union of all the sets in `S`.
More concisely: If every set in a collection of lower sets over a type with a total order has the property that any element less than or equal to one of itsmembers is also a member of the set, then the union of all the sets is also a lower set.
|
isUpperSet_compl
theorem isUpperSet_compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet sᶜ ↔ IsLowerSet s
The theorem `isUpperSet_compl` states that for any type `α` with a less than or equal to order and any set `s` of type `α`, the complement of `s` is an upper set if and only if `s` is a lower set. In other words, a set is a lower set (downward-closed set) if any element less than one of its members is also a member of the set, then the complement of that set is an upper set (upward-closed set), meaning any element greater than one of the elements in the complement set is also a member of the complement set, and vice versa.
More concisely: For any type `α` with a total order and set `s` of type `α`, the complement of `s` is an upper set if and only if `s` is a lower set.
|
IsLowerSet.ordConnected
theorem IsLowerSet.ordConnected : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → s.OrdConnected := by
sorry
The theorem `IsLowerSet.ordConnected` states that for any type `α` with a preorder, if a set `s` of elements of type `α` is a lower set (meaning that for any two elements `a` and `b` in `α`, if `b` is less than or equal to `a` and `a` is in `s`, then `b` is also in `s`), then `s` is order-connected. In other words, this theorem asserts that every lower set in a preordered set is order-connected, where an order-connected set is one where for any two elements, every element between them is also in the set.
More concisely: In a preordered set, every lower set is order-connected.
|
Mathlib.Order.UpperLower.Basic._auxLemma.23
theorem Mathlib.Order.UpperLower.Basic._auxLemma.23 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (p = q) = (↑p = ↑q)
This theorem, `Mathlib.Order.UpperLower.Basic._auxLemma.23`, states that for all types `A` and `B` where `B` is a member of a set-like structure `A`, and for all `p` and `q` of type `A`, `p` is equal to `q` if and only if the underlying elements (or coercions) of `p` and `q` are equal. This theorem establishes the equivalence between equality of set-like elements and their corresponding underlying elements.
More concisely: For all types `A` and `B` with `B` an element of `A`, and all `p` and `q` in `A` of the same type as `B`, `p = q` if and only if the underlying elements of `p` and `q` are equal.
|
IsLowerSet.preimage
theorem IsLowerSet.preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
IsLowerSet s → ∀ {f : β → α}, Monotone f → IsLowerSet (f ⁻¹' s)
This theorem states that the preimage of a lower set under a monotone function is also a lower set. More specifically, given a set `s` of elements from a partially ordered type `α`, if `s` is a lower set, and we have a function `f` from a partially ordered type `β` to `α` that is monotone (meaning if `a ≤ b` then `f(a) ≤ f(b)`), then the preimage of `s` under `f` (which is the set of all elements from `β` that `f` maps into `s`) is also a lower set. In other words, if `b` is an element of this preimage and `a` is any element from `β` such that `a ≤ b`, then `a` is also in the preimage, thus making the preimage a lower set.
More concisely: If `s` is a lower set in a partially ordered type `α` and `f` is a monotone function from a partially ordered type `β` to `α`, then the preimage of `s` under `f` is a lower set in `β`.
|
BddAbove.of_lowerClosure
theorem BddAbove.of_lowerClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove ↑(lowerClosure s) → BddAbove s
This theorem, also known as an alias for the forward direction of `bddAbove_lowerClosure`, states that for any set `s` of a certain type `α` equipped with a preorder, if the lower closure of `s` is bounded above, then `s` itself is bounded above. In mathematical terms, if there exists an upper bound for all elements in the lower closure of `s` (i.e., all elements less than or equal to any element in `s`), then there also exists an upper bound for all elements in `s`.
More concisely: If a preordered set `s` of type `α` has a bounded above lower closure, then `s` itself is bounded above.
|
isUpperSet_iUnion₂
theorem isUpperSet_iUnion₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {f : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), IsUpperSet (f i j)) → IsUpperSet (⋃ i, ⋃ j, f i j)
The theorem `isUpperSet_iUnion₂` states that for any type `α` that has a less-than-or-equal-to (`LE`) relation, and for any functions `f` that maps elements from types `ι` and `κ` to sets of `α`, if each set `f i j` is an upper set (that is, for any elements `a` and `b` of the set, if `a` is less than or equal to `b`, then `b` is also in the set), then the union of all such sets (for all `i` in `ι` and `j` in `κ i`) is also an upper set. This means that any element greater than a member of the union set is also a member of the union set.
More concisely: If `f i j` is an upper set for each `i` in `ι` and `j` in `κ`, then the union of all `f i j` is an upper set.
|
upperClosure_iUnion
theorem upperClosure_iUnion :
∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] (f : ι → Set α),
upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i)
The theorem `upperClosure_iUnion` states that for any type `α` with a preorder structure and a function `f` from some index set `ι` to the set of `α`, the upper closure of the union over `f i` for all `i` in `ι` is equivalent to the infimum of the upper closures of `f i` for all `i` in `ι`. In simpler terms, it says that the smallest upper bound containing all elements of a union of sets is the same as the smallest upper bound of all upper bounds of the individual sets.
More concisely: For any preordered type `α` and function `f` from an index set `ι` to `α`, the upper closure of the union of images `{f i | i ∈ ι}` is equal to the infimum of the upper closures of `{f i | i ∈ ι}`.
|
LowerSet.coe_iSup₂
theorem LowerSet.coe_iSup₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
↑(⨆ i, ⨆ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
This theorem, `LowerSet.coe_iSup₂`, states that for any type `α`, any `ι`-indexed type `κ` and any function `f` that maps an index `i : ι` and value `j : κ i` to a `LowerSet` of `α`, the supremum (least upper bound) of the double-indexed family of `LowerSet`s, coerced to a set, is equal to the union over all `i` and `j` of the sets given by coercing each `LowerSet (f i j)`. In simple terms, it says that the set-theoretic union of these lower sets corresponds to their supremum in the order-theoretic sense.
More concisely: For any type `α`, `ι-indexed` type `κ` and function `f : ι × κ → LowerSet α`, the coercion of the supremum of `{coe (f i j) | i ∈ ι, j ∈ κ}` to a set equals the union of `{coe (f i j) | i ∈ ι, j ∈ κ}`.
|
gc_lowerClosure_coe
theorem gc_lowerClosure_coe : ∀ {α : Type u_1} [inst : Preorder α], GaloisConnection lowerClosure SetLike.coe := by
sorry
This theorem states that for any type `α` which has a `Preorder` structure, there exists a Galois connection between the function `lowerClosure` and the function `SetLike.coe`. In other words, for every `a` in `α` and `b` in the set of lower sets, `lowerClosure a` is less than or equal to `b` if and only if `a` is less than or equal to `SetLike.coe b`. In terms of lattice theory, this is stating that the function which maps a set to the least lower set containing it and the function that maps a lower set to its corresponding set form a Galois connection.
More concisely: For any type `α` with a `Preorder` structure, the functions `lowerClosure` and `SetLike.coe` define a Galois connection.
|
UpperSet.upper
theorem UpperSet.upper : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), IsUpperSet ↑s
This theorem states that for every type `α` with an order relation (denoted by `≤`), any upper set `s` is indeed an upper set. In terms of order theory, this means that if `s` is a subset of `α` such that every element in `s` is less than or equal to any element from `α`, then `s` is considered an upper set. An upper set is defined as a set where if an element `a` is in the set and `a` is less than or equal to another element `b`, then `b` is also in the set.
More concisely: For any type `α` with an order relation `≤`, every subset `s` such that `x ∈ s` implies `x ≤ y` for all `y ∈ α`, is an upper set.
|
isLowerSet_iInter₂
theorem isLowerSet_iInter₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {f : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), IsLowerSet (f i j)) → IsLowerSet (⋂ i, ⋂ j, f i j)
The theorem `isLowerSet_iInter₂` states that, for all types `α` and `ι`, and for each function `κ` from `ι` to some other type, if `α` has an order relation (represented by `LE α`) and `f` is a function that for each `ι` and `κ i` returns a set of `α` which is a lower set (i.e., a set where for any two elements `a` and `b` of `α`, if `b` is less than or equal to `a` and `a` is in the set, then `b` is also in the set), then the intersection over all `ι` and `κ i` of the sets `f i j` is also a lower set.
In simpler terms, if you have a family of sets of some ordered type, where each of the sets is "downwards closed" (if an element is in the set, all lesser elements are too), then the intersection of all these sets also has this "downward closure" property.
More concisely: If `α` is an ordered type, and `f ι : ι → sets α` is a family of lower sets, then the intersection over all `ι` and `κ i` of the sets `f i κ` is also a lower set.
|
subset_lowerClosure
theorem subset_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s ⊆ ↑(lowerClosure s)
This theorem states that for any given set `s` of a type `α` that has a preorder relation, `s` is a subset of the lower closure of `s`. In other words, every element in `s` is also an element in the lower closure of `s`. The lower closure of a set is defined as the set of all elements that are less than or equal to some element in the original set.
More concisely: For any set `s` of type `α` with a preorder relation, `s` is a subset of the lower closure of `s`. Alternatively, every element in `s` is less than or equal to some element in `s`, so `s` is included in the set of elements that are less than or equal to elements in `s`.
|
upperClosure_singleton
theorem upperClosure_singleton : ∀ {α : Type u_1} [inst : Preorder α] (a : α), upperClosure {a} = UpperSet.Ici a := by
sorry
This theorem states that for any given element 'a' in a preordered set 'α', the greatest upper set (upperClosure) containing just that element '{a}' is equivalent to the smallest upper set (UpperSet.Ici) that contains 'a'. Here, an upper set is a subset of some preordered set, in which, if an element is included then all greater elements are also included.
More concisely: The greatest upper set containing just the element 'a' in a preordered set equals the smallest upper set that contains 'a'. In other words, upperClosure {'a'} = UpperSet.Ici 'a'.
|
IsUpperSet.inter
theorem IsUpperSet.inter :
∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsUpperSet s → IsUpperSet t → IsUpperSet (s ∩ t)
The theorem `IsUpperSet.inter` states that for any type `α` which has a less than or equal to order (`LE`) and for any two sets `s` and `t` of type `α`, if both `s` and `t` are upper sets (meaning for each of them, any element greater than or equal to one of its members is also a member), then their intersection (the set of elements common to both `s` and `t`) is also an upper set. In other words, if you have two sets where each set has the property that any element in the set that is less or equal to another element implies that the larger element is also in the set, this property is preserved in the intersection of the two sets.
More concisely: If `α` is a type with a LE relation, and `s` and `t` are upper sets of `α`, then their intersection `s ∩ t` is also an upper set.
|
IsUpperSet.ofDual
theorem IsUpperSet.ofDual :
∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsUpperSet s → IsLowerSet (⇑OrderDual.toDual ⁻¹' s)
This theorem, named `IsUpperSet.ofDual`, states that for any type `α` that has a less than or equal to (`LE`) order and any set `s` of `OrderDual` of `α` that is an upper set (an upper set is a set where any element greater than one of its members is also a member), the preimage of `s` under the dual order map (obtained via `OrderDual.toDual`) is a lower set. Here, a lower set is a set in which any element less than one of its members is also a member. Essentially, this theorem is explaining how upper sets in the dual order correspond to lower sets in the original order.
More concisely: For any type `α` with a total order `LE`, if `s` is an upper set of `OrderDual α` then the preimage of `s` under `OrderDual.toDual` is a lower set in `α`.
|
LowerSet.lower'
theorem LowerSet.lower' : ∀ {α : Type u_6} [inst : LE α] (self : LowerSet α), IsLowerSet self.carrier
This theorem states that for any `LowerSet` in a given ordered type `α`, its carrier set is a lower set. In other words, for any two elements `a` and `b` of the ordered type `α`, if `b` is less than or equal to `a` and `a` is an element of the carrier set of the `LowerSet`, then `b` is also an element of the same carrier set. This reflects the definition of a lower set, also known as a down-set or a downward-closed set, in an ordered set.
More concisely: For any `LowerSet` in an ordered type `α`, the carrier set is a lower set, i.e., for all `a` and `b` in `α` with `b ≤ a` and `a` in the carrier set, it follows that `b` is also in the carrier set.
|
Mathlib.Order.UpperLower.Basic._auxLemma.94
theorem Mathlib.Order.UpperLower.Basic._auxLemma.94 :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {x : α}, (x ∈ upperClosure s) = ∃ a ∈ s, a ≤ x
This theorem, `Mathlib.Order.UpperLower.Basic._auxLemma.94`, states that for any type `α` that has a preorder, for any set `s` of type `α`, and for any element `x` of type `α`, `x` is in the upper closure of `s` if and only if there exists an element `a` in `s` such that `a` is less than or equal to `x`. In other words, the upper closure of a set `s` is the set of all elements that are greater than or equal to at least one element in `s`.
More concisely: For any preordered type `α` and set `s` in `α`, an element `x` belongs to the upper closure of `s` if and only if there exists an element `a` in `s` such that `a ≤ x`.
|
BddAbove.lowerClosure
theorem BddAbove.lowerClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s → BddAbove ↑(lowerClosure s)
The theorem `BddAbove.lowerClosure` states that for any type `α` that has a preorder structure and for any set `s` of this type, if the set `s` is bounded above, then the lower closure of this set is also bounded above. The lower closure of a set is defined as the set of all elements which are less than or equal to at least one element in the original set. The term "bounded above" means that there exists an upper bound for the set.
More concisely: If `α` is a type with a preorder structure and `s ⊆ α` is a boundedly above set, then the lower closure of `s` is also boundedly above.
|
lowerClosure_singleton
theorem lowerClosure_singleton : ∀ {α : Type u_1} [inst : Preorder α] (a : α), lowerClosure {a} = LowerSet.Iic a := by
sorry
This theorem, `lowerClosure_singleton`, states that for any type `α` that has a preorder relation, and for any element `a` of type `α`, the lower closure of the set containing only `a` is equivalent to the principal lower set of `a`. In other words, for any element `a`, the smallest set that contains `a` and all elements less than or equal to `a` is the same set as the set of all elements less than or equal to `a`.
More concisely: For any preordered type `α` and element `a` in `α`, the lower closure of the singleton set `{a}` equals the principal lower set of `a`.
|
UpperSet.upper'
theorem UpperSet.upper' : ∀ {α : Type u_6} [inst : LE α] (self : UpperSet α), IsUpperSet self.carrier
This theorem states that the carrier of an `UpperSet` in an ordered structure `α` is an upper set. In other words, for any `UpperSet` in the type `α` where `α` has a `LE` (less than or equal to) relation, its carrier (the set it encapsulates) is an upper set. An upper set is a set in which, if it contains an element `a` and `a` is less than or equal to another element `b`, then it also contains `b`.
More concisely: If `X` is an `UpperSet` in an ordered type `α`, then the carrier of `X` is an upper set, that is, for all `a` and `b` in `α`, if `a` is in the carrier of `X` and `a` ≤ `b`, then `b` is in the carrier of `X`.
|
IsLowerSet.ofDual
theorem IsLowerSet.ofDual :
∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsLowerSet s → IsUpperSet (⇑OrderDual.toDual ⁻¹' s)
This theorem, `IsLowerSet.ofDual`, states that for any type `α` that has a less-than-or-equal-to order (`LE α`), and any set `s` of the dual order of `α` (`Set αᵒᵈ`), if `s` is a lower set (meaning, it is a set such that any element less than one of its members is also a member), then the preimage of `s` under the identity function to the dual of a linear order (`OrderDual.toDual`) is an upper set (meaning, it is a set such that any element greater than one of its members is also a member). In other words, the theorem establishes a connection between lower sets in a dual order and upper sets in the original order through the use of the identity function to the dual of a linear order.
More concisely: If `α` is a type with a linear order `LE α` and `s` is a lower set in the dual order `Set αᵒᵈ`, then the preimage of `s` under the identity function to the dual order `OrderDual.toDual` is an upper set in `α`.
|
IsLowerSet.inter
theorem IsLowerSet.inter :
∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsLowerSet s → IsLowerSet t → IsLowerSet (s ∩ t)
The theorem `IsLowerSet.inter` states that for any type `α` with a less than or equal to order (`LE α`), if `s` and `t` are both lower sets, then the intersection of `s` and `t` (denoted as `s ∩ t`) is also a lower set. In other words, if any element is less than or equal to an element in both `s` and `t`, then that element is also included in the intersection of `s` and `t`.
More concisely: If `s` and `t` are lower sets of type `α` with a total order, then `s ∩ t` is also a lower set.
|
Mathlib.Order.UpperLower.Basic._auxLemma.43
theorem Mathlib.Order.UpperLower.Basic._auxLemma.43 :
∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] {a : α} {f : ι → UpperSet α}, (a ∈ ⨆ i, f i) = ∀ (i : ι), a ∈ f i
This theorem states that for any type `α`, any type `ι`, any element `a` of type `α`, and any function `f` from `ι` to the upper sets of `α`, the condition of `a` being in the superset (denoted by `⨆`) of all `f i` is equivalent to `a` being in `f i` for every `i` in `ι`. In more human-friendly terms, an element is in the superset of all values of a function if and only if it is in the value of the function for every possible input.
More concisely: For any type `α`, any type `ι`, any element `a` of type `α`, and any function `f` from `ι` to the upper sets of `α`, `a` belongs to the supremum of `{f i | i ∈ ι}` if and only if `a` belongs to `f i` for all `i` in `ι`.
|
BddBelow.upperClosure
theorem BddBelow.upperClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow s → BddBelow ↑(upperClosure s)
The theorem `BddBelow.upperClosure` states that for any type `α` with a preorder relation and for any set `s` of type `α`, if the set `s` is bounded below, then the upper closure of `s` is also bounded below. Here, a set is said to be bounded below if there exists a lower bound for the set, and the upper closure of a set is defined as the greatest upper set containing the given set.
More concisely: If a set in a type with a preorder relation is bounded below, then its upper closure is also bounded below.
|
LowerSet.coe_iSup
theorem LowerSet.coe_iSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), ↑(⨆ i, f i) = ⋃ i, ↑(f i)
This theorem states that for any type `α`, any sort `ι`, and any function `f` from `ι` to the LowerSet of `α`, the supremum (`⨆ i, f i`) of the `f` expressed in terms of `ι`, when coerced (`↑`), equals the union (`⋃ i, ↑(f i)`) of the individual coerced values of `f i`. In simpler terms, in the context of order theory, this theorem asserts that the supremum of a collection of lower sets is equivalent to the union of those individual lower sets.
More concisely: For any type `α` and sort `ι`, the supremum of a function from `ι` to the LowerSet of `α` equals the union of the images of that function.
|
IsLowerSet.image
theorem IsLowerSet.image :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
IsLowerSet s → ∀ (f : α ≃o β), IsLowerSet (⇑f '' s)
The theorem `IsLowerSet.image` states that for any types α and β, given a preorder (an order that is reflexive and transitive) on both α and β, if we have a set `s` on α that is a lower set (meaning, for any two elements in the set, if one is less than or equal to the other, the lesser one is also in the set), then the image of `s` under any order-preserving bijection `f` from α to β is also a lower set in β. This means that the property of being a lower set is preserved under an order-preserving bijection.
More concisely: Given a preorder on types α and β, if s is a lower set on α and f is an order-preserving bijection from α to β, then the image of s under f is a lower set on β.
|
isLowerSet_compl
theorem isLowerSet_compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet sᶜ ↔ IsUpperSet s
This theorem states that for any set `s` in an ordered type `α`, the complement of `s` is a lower set if and only if `s` itself is an upper set. In other words, the complement of an upper set is always a lower set and vice-versa. This is the case regardless of the specific elements in `s` or the specific ordering of the type `α`.
More concisely: For any set `s` in a type `α` with an ordering, `s` is an upper set if and only if the complement of `s` is a lower set.
|
UpperSet.coe_iInf₂
theorem UpperSet.coe_iInf₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → UpperSet α),
↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
This theorem states that for any type `α` with a less-than-or-equal-to relation (`LE α`), and for any type-dependent function `f` that maps every element of type `ι` and its dependent type `κ i` to an upper set of `α`, the intersection of all upper sets obtained by `f` is equivalent to the union of the individual upper sets. In other words, the co-domain of the infimum operation (`⨅`) applied to `f` is equal to the union (`⋃`) of the co-domains of the individual sets produced by `f`.
More concisely: For any type `α` with a `LE` relation and any type-dependent function `f` mapping each `ι i` and its dependent type `κ i` to an upper set of `α`, the infimum of the `f i`'s upper sets equals the union of their co-domains.
|
LowerSet.lower
theorem LowerSet.lower : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), IsLowerSet ↑s
This theorem states that for any type `α` that has a less than or equal to (`LE`) relationship, and for any lower set `s` of type `α`, `s` is a lower set. In other words, if `s` is a lower set of a certain type, then any element less than or equal to another element in `s` is also a member of `s`.
More concisely: If `α` is a type with a `LE` relation, and `s` is a lower set of `α`, then for all `x y ∈ s`, `x LE y` implies `x ∈ s`.
|
LowerSet.coe_iInf
theorem LowerSet.coe_iInf :
∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), ↑(⨅ i, f i) = ⋂ i, ↑(f i)
This theorem, `LowerSet.coe_iInf`, states that for any type `α` and any sort `ι`, given an operation `LE` on `α` and a function `f` that maps `ι` to a lower set of `α`, the coercion of the greatest lower bound (infimum or `⨅`) of the function `f` over all `ι` is equal to the intersection over all `ι` of the coercion of the function `f`. In other words, it equates the infimum of a collection of lower sets to the intersection of the sets themselves.
More concisely: Given an operation LE on type α and a function f from sort ι to lower sets of α, the coercion of the inf (⨅) of the images of f is equal to the intersection of the coercions of the images.
|
BddBelow.of_upperClosure
theorem BddBelow.of_upperClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow ↑(upperClosure s) → BddBelow s
This theorem, termed as an alias of the forward direction of `bddBelow_upperClosure`, states that for any type `α` that has a preorder (i.e., a binary relation that is reflexive and transitive), and for any set `s` of that type, if the upper closure of set `s` (which is the greatest upper set containing set `s`) is bounded below, then set `s` itself is also bounded below. In other words, if there exists a lower bound for all elements in the upper closure of a set, then there is also a lower bound for all elements in the original set itself.
More concisely: If a preordered type's upper closure of a set has a lower bound, then the set itself has a lower bound.
|
gc_upperClosure_coe
theorem gc_upperClosure_coe :
∀ {α : Type u_1} [inst : Preorder α],
GaloisConnection (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)
This theorem states that for any type `α` that has a `Preorder` instance, there exists a Galois connection between two functions. The first function is composed of `OrderDual.toDual` and `upperClosure` while the second function is composed of `SetLike.coe` and `OrderDual.ofDual`. In other words, for all elements `a` and `b`, passing `a` through the first function and comparing it with `b` using the `≤` comparison is equivalent to comparing `a` with the result of passing `b` through the second function, again using the `≤` comparison. The functions `OrderDual.toDual` and `OrderDual.ofDual` are essentially identity functions over the order dual of a linear order. `upperClosure` gives the greatest upper set containing a given set, and `SetLike.coe` is a coercion from a term of a `SetLike` to its corresponding `Set`.
More concisely: For any type `α` with a `Preorder` instance, the functions `OrderDual.toDual ∘ upperClosure` and `SetLike.coe ∘ OrderDual.ofDual` define a Galois connection, i.e., for all `a` and `b`, `a ≤ b` if and only if `upperClosure a ≤ b` if and only if `a ≤ SetLike.coe (OrderDual.ofDual b)`.
|
upperBounds_lowerClosure
theorem upperBounds_lowerClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, upperBounds ↑(lowerClosure s) = upperBounds s
The theorem `upperBounds_lowerClosure` states that for any set `s` of elements of a given type `α` in a preordered set, the set of upper bounds of the least lower set containing `s` (i.e., the lower closure of `s`) is equal to the set of upper bounds of `s` itself. In other words, all elements that are greater than or equal to every element of `s` are also greater than or equal to every element in the least lower set containing `s`, and vice versa.
More concisely: The theorem `upperBounds_lowerClosure` asserts that the set of upper bounds of a set in a preordered set equals the set of upper bounds of its lower closure.
|
lowerClosure_min
theorem lowerClosure_min :
∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsLowerSet t → ↑(lowerClosure s) ⊆ t
The theorem `lowerClosure_min` states that for any type `α` having a preorder structure and any sets `s` and `t` of this type, if `s` is a subset of `t` and `t` is a lower set (i.e., for any elements `a` and `b` in `t`, if `b` is less than or equal to `a`, then `b` is also in `t`), then the lower closure of `s` (which is the least lower set containing `s`) is also a subset of `t`. It essentially says that the smallest lower set containing `s` is contained within any lower set that contains `s`.
More concisely: If `s` is a subset of a lower set `t` in a preordered type `α`, then the lower closure of `s` is included in `t`.
|
Mathlib.Order.UpperLower.Basic._auxLemma.41
theorem Mathlib.Order.UpperLower.Basic._auxLemma.41 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B}, (x ∈ ↑p) = (x ∈ p)
This theorem states that for any types `A` and `B`, given a SetLike instance `i` from `A` to `B`, and for any `p` of type `A` and `x` of type `B`, belonging of `x` to the coercion of `p` to a set is equivalent to belonging of `x` to `p` itself. In other words, `x` is in `p` if and only if `x` is in the set obtained by coercing `p` to a set.
More concisely: For any SetLike instance from type `A` to type `B`, and for any `p` of type `A` and `x` of type `B`, `x` belongs to `p` if and only if `x` belongs to the coercion of `p` to a set.
|
Mathlib.Order.UpperLower.Basic._auxLemma.95
theorem Mathlib.Order.UpperLower.Basic._auxLemma.95 :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {x : α}, (x ∈ lowerClosure s) = ∃ a ∈ s, x ≤ a
This theorem states that for any type `α`, which has a preorder relation, any set `s` of type `α`, and any element `x` of type `α`, `x` belongs to the lower closure of the set `s` if and only if there exists an element `a` in the set `s` such that `x` is less than or equal to `a`. That is, the lower closure of a set `s` includes any element `x` that is less than or equal to some element `a` in `s`.
More concisely: For any preordered type `α` and set `s` of `α`, an element `x` belongs to the lower closure of `s` if and only if there exists `a` in `s` such that `x ≤ a`.
|
lowerClosure_iUnion
theorem lowerClosure_iUnion :
∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] (f : ι → Set α),
lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i)
This theorem states that for any type `α` with a preorder relation, and any indexed family `f` of sets of `α` indexed by `ι`, the least lower set that contains the union of sets given by `f` is equal to the supremum of the least lower sets of each set in the family `f`. In other words, the lower closure operation distributes over the union operation, which can alternatively be viewed as the supremum of the lower closures being equal to the lower closure of the unions.
More concisely: For any type `α` with a preorder relation, and any indexed family `f` of subsets of `α` indexed by `ι`, the lower closure of the union of `f` is equal to the supremum of the lower closures of each set in `f`.
|
UpperSet.ext
theorem UpperSet.ext : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, ↑s = ↑t → s = t
This theorem, `UpperSet.ext`, states that for any type `α` with a less than or equal to (`≤`) relation, given two upper sets `s` and `t` of type `α`, if the coercion (or the underlying set) of `s` is equal to the coercion of `t`, then `s` is equal to `t`. An upper set is a set of elements in which any element that is greater than or equal to any element in the set is also in the set.
More concisely: If two upper sets of a type with a `≤` relation have equal underlying sets, then they are equal.
|
IsUpperSet.preimage
theorem IsUpperSet.preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
IsUpperSet s → ∀ {f : β → α}, Monotone f → IsUpperSet (f ⁻¹' s)
The theorem `IsUpperSet.preimage` states that for all types `α` and `β` with a preorder (a reflexive and transitive binary relation), given an upper set `s` (a set in which if an element is a member, then any element greater than it is also a member) in `α`, and a monotone function `f` from `β` to `α` (a function such that if `a ≤ b` then `f(a) ≤ f(b)`), the preimage of `s` under `f` (the set of all elements in `β` that `f` maps into `s`) is also an upper set. In other words, the monotone preimage of an upper set is also an upper set in the context of preordered sets.
More concisely: If `s` is an upper set in a preordered type `α` and `f` is a monotone function from a preordered type `β` to `α`, then the preimage of `s` under `f` is an upper set in `β`.
|
subset_upperClosure
theorem subset_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s ⊆ ↑(upperClosure s)
This theorem, `subset_upperClosure`, states that for any set `s` in a pre-ordered type `α`, `s` is a subset of the upper closure of `s`. In other words, all elements of set `s` are also elements of the upper closure of `s`. The upper closure of a set is defined as the greatest upper set containing the given set, meaning it includes all elements from the original set and possibly additional elements that are greater than or equal to some element in `s` according to the preorder.
More concisely: For any pre-ordered set `α` and set `s` in `α`, `s` is a subset of the upper closure of `s`. (i.e., all elements of `s` are in the upper closure of `s`).
|
IsLowerSet.Iic_subset
theorem IsLowerSet.Iic_subset :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s
This theorem, referred to as `IsLowerSet.Iic_subset`, states that for any type `α` with a preorder relation, and for any set `s` of type `α` that is a lower set, for every element `a` in `s`, the left-infinite right-closed interval of `a` (denoted as `Set.Iic a`) is a subset of `s`. In other words, if `s` is a lower set in some ordered set, then any interval extending to negative infinity up to any element `a` from `s` is also contained within `s`.
More concisely: For any type `α` with a preorder relation and any lower set `s` in `α`, for all `a` in `s`, we have `Set.Iic a ⊆ s`, where `Set.Iic a` denotes the left-infinite right-closed interval of `a`.
|
IsUpperSet.Ici_subset
theorem IsUpperSet.Ici_subset :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s
The theorem `IsUpperSet.Ici_subset` states that for any type `α` with a preorder, if a set `s` is an upper set, then for any element `a` in `s`, the interval from `a` to infinity (`Set.Ici a`) is a subset of `s`. In simpler terms, if a set includes all elements greater than any of its members, then starting from any member of the set and going towards infinity, all those elements are contained within the set.
More concisely: If `s` is an upper set of a preordered type `α`, then `s ⊆ Set.Ici a` for all `a ∈ s`.
|
Mathlib.Order.UpperLower.Basic._auxLemma.45
theorem Mathlib.Order.UpperLower.Basic._auxLemma.45 :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b = (a ⊓ b = ⊥)
This theorem states that, for any type `α` which has a structure of a semilattice with respect to an infimum operation and also has a least or "bottom" element, and for any two elements `a` and `b` of this type, `a` and `b` are disjoint if and only if the infimum of `a` and `b` is the bottom element. In mathematical terms, it says that $a$ and $b$ are disjoint (which is defined as that for any $x$ that is less than or equal to both $a$ and $b$, $x$ must also be less than or equal to the bottom element) if and only if $a \wedge b = \bot$, where $\wedge$ denotes the infimum operation and $\bot$ represents the bottom element.
More concisely: For any semilattice with a least element, elements $a$ and $b$ are disjoint if and only if their infimum is the least element.
|
IsUpperSet.toDual
theorem IsUpperSet.toDual :
∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet s → IsLowerSet (⇑OrderDual.ofDual ⁻¹' s)
The theorem `IsUpperSet.toDual` states that for any type `α` equipped with a less-than-or-equal-to order (`LE α`), and any set `s` of this type, if `s` is an upper set -- i.e., any element greater than a member of the set is also a member of the set -- then the preimage of `s` under the identity function of the order dual of `α` is a lower set. This means that any element less than a member of the preimage set (which consists of elements from `s`) is also a member of the preimage set. This theorem essentially shows that the concept of an upper set in an order can be transformed into the concept of a lower set in the dual order by applying the identity function of the dual order and considering the preimage of the original set.
More concisely: For any type `α` with a order `LE α` and any upper set `s` of `α`, the preimage of `s` under the identity function of `α`'s dual order is a lower set.
|
isUpperSet_iInter₂
theorem isUpperSet_iInter₂ :
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {f : (i : ι) → κ i → Set α},
(∀ (i : ι) (j : κ i), IsUpperSet (f i j)) → IsUpperSet (⋂ i, ⋂ j, f i j)
The `isUpperSet_iInter₂` theorem states that for any type `α` that has a less than or equal to (`≤`) relation, and for any two indexed families `{ι : Sort u_4}` and `{κ : ι → Sort u_5}`, if for every index `i` from `ι` and `j` from `κ i`, the set `f i j` is an upper set, then the intersection of all these sets (expressed as `(⋂ i, ⋂ j, f i j)`) is also an upper set. In other words, the intersection of any collection of upper sets is itself an upper set.
More concisely: If for every index `i` and `j`, `f i j` is an upper set, then their intersection `(⋂ i, ⋂ j, f i j)` is also an upper set.
|
Mathlib.Order.UpperLower.Basic._auxLemma.85
theorem Mathlib.Order.UpperLower.Basic._auxLemma.85 :
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (b ∈ LowerSet.Iic a) = (b ≤ a)
The theorem `Mathlib.Order.UpperLower.Basic._auxLemma.85` states that for any type `α` equipped with a preorder and for any elements `a` and `b` of type `α`, `b` is a member of the principal lower set of `a` (`LowerSet.Iic a`) if and only if `b` is less than or equal to `a`. In other words, the membership of `b` in the principal lower set of `a` is equivalent to the inequality `b ≤ a`.
More concisely: For any preordered type `α` and elements `a` and `b` of `α`, `b` belongs to the principal lower set of `a` if and only if `b` is less than or equal to `a`.
|
IsLowerSet.compl
theorem IsLowerSet.compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet s → IsUpperSet sᶜ
This theorem states that for any type `α` equipped with a less than or equal to (`≤`) relation, and for any set `s` of elements of type `α`, if `s` is a lower set (i.e., for any elements `a` and `b` of type `α`, if `b` is less than or equal to `a` and `a` is in `s`, then `b` is also in `s`), then the complement of `s` (denoted as `sᶜ`) is an upper set (i.e., for any elements `a` and `b` of type `α`, if `a` is less than or equal to `b` and `a` is in `sᶜ`, then `b` is also in `sᶜ`). In other words, the complement of a lower set is an upper set.
More concisely: If `s` is a lower set of type `α`, then the complement `sᶜ` is an upper set.
|
Set.OrdConnected.upperClosure_inter_lowerClosure
theorem Set.OrdConnected.upperClosure_inter_lowerClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected → ↑(upperClosure s) ∩ ↑(lowerClosure s) = s := by
sorry
This theorem states that for any set `s` of elements of a certain type `α`, under the condition that `α` has a Preorder relation and the set `s` is order-connected, the intersection of the upper closure and lower closure of `s` is equivalent to `s` itself. In other words, for an order-connected set, the overlap of all elements that are at least as great as some element in the set and all elements that are at most as great as some element in the set, is nothing but the set itself.
More concisely: For any order-connected subset `s` of a preordered type `α`, the upper and lower closures of `s` coincide, i.e., `s` = `cl_upper s` = `cl_lower s`.
|
lowerBounds_upperClosure
theorem lowerBounds_upperClosure :
∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, lowerBounds ↑(upperClosure s) = lowerBounds s
This theorem states that for any given set `s` of a certain type `α` that obeys a preorder (i.e., a binary relation that is reflexive and transitive), the set of lower bounds of the upper closure of `s` is equal to the set of lower bounds of `s` itself. In other words, the set of all elements that are less than or equal to all elements in the upper closure of `s` is the same as the set of all elements that are less than or equal to all elements in `s`.
More concisely: For any set `s` of type `α` in a preorder, the set of lower bounds of `s` is equal to the set of lower bounds of its upper closure.
|
LowerSet.ext
theorem LowerSet.ext : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, ↑s = ↑t → s = t
This theorem, named `LowerSet.ext`, asserts that for any type `α` with a less-than-or-equal-to (`LE`) order relation, if two lower sets `s` and `t` of this type have the same elements (i.e., `↑s = ↑t`), then they are the same lower set (`s = t`). A lower set is a set of elements such that, if an element is in the set, then all lesser elements are also in the set. Therefore, this theorem is essentially saying that two lower sets are equal if and only if they contain the same elements.
More concisely: If `α` is a type with a `LE` order relation and `s` and `t` are lower sets of `α` with the same elements, then `s = t`.
|
IsLowerSet.toDual
theorem IsLowerSet.toDual :
∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsLowerSet s → IsUpperSet (⇑OrderDual.ofDual ⁻¹' s)
The theorem `IsLowerSet.toDual` states that for any type `α` with a less-than-or-equal-to order `LE α` and any set `s` of type `α`, if `s` is a lower set (i.e., a set for which any element less than one of its members is also a member), then the preimage of `s` under the identity function of the dual order is an upper set (i.e., a set for which any element greater than one of its members is also a member). This theorem is essentially a rephrasing of the reverse direction of the theorem `isUpperSet_preimage_ofDual_iff`.
More concisely: If `s` is a lower set in a type `α` with order `LE α`, then the preimage of `s` under the identity function of the dual order is an upper set.
|
IsUpperSet.compl
theorem IsUpperSet.compl : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsUpperSet s → IsLowerSet sᶜ
The theorem `IsUpperSet.compl` states that for any type `α` with an order relation and any set `s` of elements of type `α`, if `s` is an upper set (meaning that any element of `s` greater than another element is also in `s`), then the complement of `s` (denoted by `sᶜ`, which consists of all the elements of type `α` that are not in `s`) is a lower set (meaning that any element of `sᶜ` less than another element is also in `sᶜ`). In mathematical terms, it is saying that the complement of an upward-closed set in an ordered set is a downward-closed set.
More concisely: If `s` is an upper set in an ordered type `α`, then the complement `sᶜ` is a lower set.
|
IsUpperSet.image
theorem IsUpperSet.image :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
IsUpperSet s → ∀ (f : α ≃o β), IsUpperSet (⇑f '' s)
The theorem `IsUpperSet.image` states that for any two types `α` and `β` which are both pre-ordered sets, and a set `s` in `α` which is an upper set, if there is an order-preserving bijection `f` from `α` to `β`, then the image of `s` under `f` is also an upper set in `β`. In other words, the image of an upper set under an order-preserving bijection remains an upper set.
More concisely: If `α` and `β` are pre-ordered sets, `s` is an upper set in `α`, and `f` is an order-preserving bijection from `α` to `β`, then the image `f''(s)` is an upper set in `β`.
|