sup_bot_eq
theorem sup_bot_eq : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α), a ⊔ ⊥ = a
This theorem states that for any type `α` that is a semilattice with a supremum operation and has a least element `⊥`, the supremum of any element `a` of `α` and `⊥` is equal to `a`. This essentially means that the least element `⊥` does not affect the supremum operation, confirming the property of `⊥` as the least element in the ordered set.
More concisely: For any semilattice `α` with a least element `⊥`, the supremum of any element `a` in `α` and `⊥` is equal to `a`.
|
ne_bot_of_le_ne_bot
theorem ne_bot_of_le_ne_bot :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, b ≠ ⊥ → b ≤ a → a ≠ ⊥
This theorem states that for any type `α` which has a partial order and a least element (denoted by `⊥`), if `b` is not equal to this least element (`⊥`) and `b` is less than or equal to `a`, then `a` is also not equal to the least element (`⊥`). The theorem essentially says that if `a` is greater than or equal to an element that is not the smallest possible, then `a` cannot be the smallest possible element itself.
More concisely: If `α` is a type with a partial order and a least element `⊥`, then for all `a` and `b` in `α`, if `b ≤ a` and `b ≠ ⊥`, then `a ≠ ⊥`.
|
le_bot_iff
theorem le_bot_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≤ ⊥ ↔ a = ⊥
This theorem, `le_bot_iff`, states that for any type `α` equipped with a partial order and a least element (denoted `⊥`), a given element `a` of type `α` is less than or equal to the least element if and only if `a` is in fact the least element itself. In other words, in such a system, the only element that is less than or equal to the least element is the least element itself.
More concisely: For any type equipped with a partial order and a least element, an element is less than or equal to the least element if and only if they are equal.
|
isMax_top
theorem isMax_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α], IsMax ⊤
The theorem `isMax_top` states that for any given type `α` equipped with a preorder (a binary relation that is reflexive and transitive) and an order top (a greatest element), the top element `⊤` (the greatest element of `α`) is a maximal element. In the context of this theorem, a maximal element is defined as an element `a` such that for any other element `b`, if `a` is less than or equal to `b`, then `b` is less than or equal to `a` - in other words, no element is strictly greater than `a`.
More concisely: For any type `α` with a preorder and an order top element `⊤`, the top element is a maximal element with no strictly greater elements.
|
isMin_iff_eq_bot
theorem isMin_iff_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsMin a ↔ a = ⊥ := by
sorry
This theorem states that, for any type `α` that has a partial order and a minimum element (`⊥`), an element `a` of `α` is a minimal element (as defined by the `IsMin` property) if and only if `a` is equal to the minimum element (`⊥`). In other words, in such a structure, the only element that satisfies the minimal element property is the designated minimum element.
More concisely: For any type `α` with a partial order and a minimum element, an element `a` is a minimal element if and only if `a = ⊥`.
|
sup_top_eq
theorem sup_top_eq : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderTop α] (a : α), a ⊔ ⊤ = ⊤
This theorem states that for any type `α` that forms a semilattice with an operation "sup" (which stands for supremum or least upper bound) and also has a top element (`⊤`), the supremum of any element `a` of type `α` and the top element is always equal to the top element. In terms of set theory, the supremum of a set and the universal set is the universal set itself. This is an instance of the general principle that in a partially ordered set, the supremum of any element and the greatest element is the greatest element.
More concisely: For any semilattice `α` with top element `⊤`, the supremum of any element `a` in `α` is equal to `⊤`.
|
LT.lt.ne_bot
theorem LT.lt.ne_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, a < b → b ≠ ⊥
This theorem, `LT.lt.ne_bot`, states that for any type `α` that has a `Preorder` and `OrderBot` instance, if `a` and `b` are elements of `α` and `a` is less than `b`, then `b` cannot be the bottom element of `α`. In other words, if one element is strictly less than another in the given ordered set, the larger element can't be the lowest possible value in that set.
More concisely: For any preordered type `α` with bottom element `bot`, if `a < b` holds in `α`, then `bot ≠ b`.
|
Mathlib.Order.BoundedOrder._auxLemma.15
theorem Mathlib.Order.BoundedOrder._auxLemma.15 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, (a ≤ ⊥) = (a = ⊥)
This theorem, named `Mathlib.Order.BoundedOrder._auxLemma.15`, states that for any type `α` that has a partial order and a bottom element (`⊥`), any element `a` of this type is less than or equal to the bottom element if and only if `a` is equal to the bottom element. This is a fundamental property of partially ordered sets with a smallest element, where anything less than or equal to the smallest element must necessarily be the smallest element itself.
More concisely: For any partially ordered type with a bottom element, an element is less than or equal to the bottom element if and only if it is equal to the bottom element.
|
eq_top_iff
theorem eq_top_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a = ⊤ ↔ ⊤ ≤ a
This theorem, `eq_top_iff`, states that for any type `α` with a partial order and a top element, a given element `a` of type `α` is equal to the top element if and only if the top element is less than or equal to `a`. This essentially provides a condition under which an element can be identified as the top element in a partially ordered set.
More concisely: For any partially ordered type `α` with a top element, an element `a` is equal to the top element if and only if the top element is less than or equal to `a`.
|
Mathlib.Order.BoundedOrder._auxLemma.12
theorem Mathlib.Order.BoundedOrder._auxLemma.12 :
∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, (a < ⊥) = False
This theorem states that for any type `α` with a preorder and a bottom element (`OrderBot`), any element `a` of `α` is not less than the bottom element. In other words, for all `a` in `α`, `a < ⊥` is always false. This aligns with the intuitive concept that the bottom element (`⊥`) is defined to be the least element in the order, so no other element can be lesser than it.
More concisely: For any type `α` with a preorder and a bottom element `⊥`, there is no element `a` in `α` such that `a` is strictly less than `⊥`.
|
sup_eq_bot_iff
theorem sup_eq_bot_iff :
∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a b : α}, a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
This theorem states that for any type `α` that is a semilattice with a supremum operation and has a bottom element, the supremum (`⊔`) of any two elements `a` and `b` of this type is equal to the bottom element if and only if both `a` and `b` are the bottom element.
More concisely: For any semilattice `α` with a bottom element, `⊔(a, b) = bottom` if and only if `a = bottom` and `b = bottom`.
|
Ne.lt_top
theorem Ne.lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a ≠ ⊤ → a < ⊤
This theorem states that for any type `α` that has a partial order (`PartialOrder α`) and a designated top element (`OrderTop α`), any element `a` of type `α` that is not equal to the top element (`a ≠ ⊤`) is less than the top element (`a < ⊤`). In mathematical terms, it means that in a partially ordered set with a greatest element, any element not equal to this greatest element is strictly less than the greatest element.
More concisely: In a partially ordered set with a top element, every element not equal to the top is strictly less than it.
|
subsingleton_of_bot_eq_top
theorem subsingleton_of_bot_eq_top :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ → Subsingleton α
This theorem states that for any type `α` that has a partial order and a bounded order, if the bottom element `⊥` is equal to the top element `⊤`, then `α` is a subsingleton. In other words, if the least and greatest elements in the ordered set are the same, then the set consists of at most one element.
More concisely: If a type `α` equipped with a partial order and a bottom element `⊥` has `⊥ = ⊤`, then `α` is a subsingleton. (In other words, an ordered set `(α, ≤, ⊥)` with a bottom element and a greatest element identical is a set with at most one element.)
|
top_ne_bot
theorem top_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : Nontrivial α], ⊤ ≠ ⊥
The theorem `top_ne_bot` states that for any type `α` with a partial order, a bounded order, and is nontrivial (i.e., it contains at least two distinct elements), the top element (denoted by `⊤`) is not equal to the bottom element (denoted by `⊥`). This implies that in any nontrivial partially ordered set that also has a greatest and least element, these two elements are distinct.
More concisely: In any nontrivial partially ordered set, the greatest element (top) is distinct from the least element (bottom).
|
OrderTop.le_top
theorem OrderTop.le_top : ∀ {α : Type u} [inst : LE α] [self : OrderTop α] (a : α), a ≤ ⊤
This Lean theorem, `OrderTop.le_top`, states that for any type `α` that has a structure of an ordered set with a greatest element (denoted by `⊤`), any element `a` of type `α` is less than or equal to `⊤`. In other words, `⊤` is the greatest element in this order structure.
More concisely: For any ordered type `α` with a greatest element `⊤`, every element `a` in `α` satisfies `a ≤ ⊤`.
|
isTop_top
theorem isTop_top : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α], IsTop ⊤
The theorem `isTop_top` states that for any type `α` that has a less than or equal to relation (`LE α`) and a greatest element (`OrderTop α`), the greatest element (denoted by `⊤`) is a top element according to the definition of `IsTop`. In other words, the greatest element is greater than or equal to any other element in `α`.
More concisely: For any type `α` equipped with a total order having a greatest element, the greatest element is a top element in the order.
|
OrderBot.bot_le
theorem OrderBot.bot_le : ∀ {α : Type u} [inst : LE α] [self : OrderBot α] (a : α), ⊥ ≤ a
This theorem states that `⊥` (the bottom element) is the least element in a partially ordered set. More formally, for any type `α` that has a less-than-or-equal-to (`LE`) relation and an `OrderBot` instance (indicating that `α` has a least element `⊥`), any element `a` of type `α` satisfies the inequality `⊥ ≤ a`.
More concisely: For any type `α` with a `LE` relation and an `OrderBot` instance, the bottom element `⊥` is less than or equal to every element `a` of type `α`.
|
le_top
theorem le_top : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α] {a : α}, a ≤ ⊤
This theorem, `le_top`, states that for any given type `α` that has a less than or equal to (`LE`) relation and a greatest element (`OrderTop`), any element `a` of type `α` is less than or equal to the greatest element (`⊤`). In other words, it's asserting that for any element in a partially ordered set with a top element, that element is always less than or equal to the top.
More concisely: For any type `α` equipped with a `LE` relation and an `OrderTop`, every element `a` in `α` satisfies `a ≤ ⊤`.
|
IsBot.eq_bot
theorem IsBot.eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsBot a → a = ⊥
This theorem, named `IsBot.eq_bot`, states that for any type `α` that has a partial order and a bottom element (`OrderBot α`), any element `a` of `α` that satisfies the `IsBot` property (i.e., it is less than or equal to any other element in `α`) is equal to the bottom element of `α` (`⊥`). The `IsBot.eq_bot` theorem is essentially an alias for the forward direction of the `isBot_iff_eq_bot` theorem.
More concisely: For any type `α` with a partial order and a bottom element `⊥`, any element `a` that satisfies `IsBot` property (i.e., `a ≤ x` for all `x` in `α`) is equal to `⊥`.
|
eq_top_or_lt_top
theorem eq_top_or_lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] (a : α), a = ⊤ ∨ a < ⊤ := by
sorry
This theorem, `eq_top_or_lt_top`, states that for any given type `α` which has a partial order and a greatest element denoted by `⊤`, any element `a` of type `α` either equals `⊤` or is less than `⊤`. In other words, for any element in a partially ordered set with a greatest element, that element is either the greatest element itself or some element lesser than the greatest one.
More concisely: For any element `a` in a partially ordered set `α` with a greatest element `⊤`, we have `a = ⊤` or `a < ⊤`.
|
bot_unique
theorem bot_unique : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≤ ⊥ → a = ⊥
This theorem, named `bot_unique`, states that for any type `α` that has a partial order and a least element (`⊥`), if any element `a` of type `α` is less than or equal to `⊥`, then `a` must be equal to `⊥`. In other words, `⊥` is the unique minimal element in the partially ordered set.
More concisely: In a partially ordered type with a least element, any element less than or equal to the least element is equal to it.
|
LT.lt.ne_top
theorem LT.lt.ne_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a ≠ ⊤
This theorem, called `LT.lt.ne_top`, states that for any type `α` with a `Preorder` and `OrderTop` structure, if a is less than b (denoted by "a < b"), then a cannot be equal to the top element (denoted by "a ≠ ⊤"). Essentially, if some element a is less than another element b in this ordered structure, a cannot be the maximum (or "top") element in this structure.
More concisely: In any preordered type with a top element, there are no elements related by the strict order relation and equal to the top element.
|
inf_bot_eq
theorem inf_bot_eq : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderBot α] (a : α), a ⊓ ⊥ = ⊥
This theorem states that for any type `α` which is a semilattice with respect to the operation of infimum (also known as 'meet' or 'greatest lower bound') and has a bottom element (the least element in the set), the infimum of any element `a` of type `α` and the bottom element is always the bottom element. In other words, in a meet-semilattice with a least element, the greatest lower bound of any element and the least element is always the least element itself.
More concisely: In a semilattice with a bottom element, the infimum of any element with the bottom element is the bottom element itself.
|
bot_lt_top
theorem bot_lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : Nontrivial α], ⊥ < ⊤
This theorem states that, for any type `α` that has a partial order, a bounded order, and is nontrivial (i.e., it has at least two distinct elements), the least element (`⊥`) is less than the greatest element (`⊤`). In other words, in any nontrivial bounded partially ordered set, the smallest element is always less than the largest element.
More concisely: In any nontrivial, bounded partially ordered set, the least element is less than the greatest element.
|
not_top_lt
theorem not_top_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, ¬⊤ < a
This theorem states that for any type `α` that has a pre-order structure and a maximum element (`OrderTop α`), there is no element `a` in `α` such that the maximum element is less than `a`. In other words, it's impossible for the top element (`⊤`) of the pre-order to be less than any element in the set, which makes sense as `⊤` is defined to be the greatest element in the set.
More concisely: For any pre-order type `α` with a maximum element `⊤`, there is no element `a` in `α` such that `⊤` is strictly less than `a`.
|
IsMax.eq_top
theorem IsMax.eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsMax a → a = ⊤
The theorem `IsMax.eq_top` states that for any type `α` that has a partial order and a greatest element (`OrderTop α`), if `a` is a maximal element in `α` (i.e., no element in `α` is strictly greater than `a`), then `a` is equal to the greatest element of `α`, denoted by `⊤`. This is essentially an alias of the forward direction of the theorem `isMax_iff_eq_top`.
More concisely: For any type `α` with a greatest element `⊤` and a partial order, a maximal element `a` equals the greatest element `⊤`.
|
bot_le
theorem bot_le : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α] {a : α}, ⊥ ≤ a
This theorem states that for any type `α` that has a `≤` (less than or equal to) operation and a bottom element `⊥` (which is the least element in the type), the bottom element is less than or equal to any element `a` of type `α`. In other words, in any ordered set with a smallest element (the bottom element), that smallest element is always less than or equal to any other element in the set.
More concisely: For any type `α` equipped with a `≤` relation and a bottom element `⊥`, we have `⊥ ≤ a` for all `a : α`.
|
IsTop.eq_top
theorem IsTop.eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsTop a → a = ⊤
The theorem `IsTop.eq_top` states that for any type `α`, with a partial order and a designated "top" element, if a particular element `a` of `α` satisfies the property `IsTop`, then `a` is equal to the top element. Here, an element `a` has the `IsTop` property if it is greater than or equal to every other element in `α`.
More concisely: For any type `α` with a partial order and a top element, an element `a` with the property `IsTop` equals the top element. In other words, `a = top` whenever `a` is greater than or equal to every element in `α`.
|
Ne.bot_lt
theorem Ne.bot_lt : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
This theorem, `Ne.bot_lt`, states that for any type `α` that is equipped with a partial ordering and a smallest (bottom) element, if `a` is an element of `α` and `a` is not equal to the bottom element, then the bottom element is less than `a`. That is, in this order, any element other than the smallest one is strictly larger than the smallest one.
More concisely: For any type `α` with a partial ordering and a smallest element `bot`, if `a` is in `α` and `a ≠ bot`, then `bot < a`.
|
Mathlib.Order.BoundedOrder._auxLemma.4
theorem Mathlib.Order.BoundedOrder._auxLemma.4 :
∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a : α}, (⊤ < a) = False
This theorem asserts that for any type `α` which has a Preorder and OrderTop (meaning it has a greatest element denoted by ⊤), and for any instance `a` of `α`, the statement that the greatest element (⊤) is less than `a` is always false. In other words, there is no element in the order that is greater than the greatest element ⊤.
More concisely: For any type equipped with a Preorder and OrderTop, the greatest element is not less than any other element.
|
lt_top_iff_ne_top
theorem lt_top_iff_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a < ⊤ ↔ a ≠ ⊤ := by
sorry
This theorem states that for any type `α`, given a partial order and an order top on `α`, and for any element `a` of type `α`, `a` is less than the top element if and only if `a` is not equal to the top element. In other words, an element in such a partially ordered set is less than the maximum (top) element if and only if it is not that maximum element itself.
More concisely: In a partially ordered set, an element is strictly less than the top element if and only if it is not the top element itself.
|
inf_top_eq
theorem inf_top_eq : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α), a ⊓ ⊤ = a
This theorem states that for any type 'α' that is a semilattice with an operation of infimum (denoted as '⊓'), and also has a top element (denoted as '⊤'), the infimum of any element 'a' in 'α' and the top element is always 'a'. In simpler terms, it states that in such a structure, taking the "minimum" (infimum) between any element and the greatest possible element (top element) will always yield the original element.
More concisely: For any semilattice 'α' with an infimum operation and top element, the infimum of any element 'a' with the top element is 'a'.
|
eq_top_mono
theorem eq_top_mono : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, a ≤ b → a = ⊤ → b = ⊤
This theorem, `eq_top_mono`, states that for any type `α` that has a partial order and a maximum or top element, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b` and `a` is the top element, then `b` must also be the top element. In simpler terms, if `a` is the maximum possible value and `b` is at least as large as `a`, then `b` must also be the maximum possible value.
More concisely: If `α` is a type with a partial order and a maximum element `m`, then `m` is unique and any element `x` with `x ≤ m` implies `m = x`.
|
top_le_iff
theorem top_le_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ⊤ ≤ a ↔ a = ⊤
This theorem states that for any type `α` that has a partial order and a greatest element (`⊤`), a given element `a` of type `α` satisfies `⊤ ≤ a` if and only if `a` is equal to `⊤`. In other words, in such a partially ordered set, the only element that the greatest element (`⊤`) is less than or equal to, is the greatest element itself.
More concisely: In a partially ordered set with a greatest element, the greatest element is the unique element that is less than or equal to itself.
|
max_eq_bot
theorem max_eq_bot :
∀ {α : Type u} [inst : LinearOrder α] [inst_1 : OrderBot α] {a b : α}, max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
This theorem states that for any type `α` that has a linear order and a least element (`OrderBot`), the maximum of any two elements `a` and `b` of `α` is the least element if and only if both `a` and `b` are the least element. In other words, in a linearly ordered set with a minimum, the maximum value of any two elements is the minimum value if and only if both elements are the minimum value.
More concisely: In a linearly ordered set with a minimum element, the maximum of any two elements is equal to the minimum if and only if both elements are minimum.
|
bot_inf_eq
theorem bot_inf_eq : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderBot α] (a : α), ⊥ ⊓ a = ⊥
The theorem `bot_inf_eq` states that for all types `α` that are equipped with a semilattice structure (`SemilatticeInf α`) and a bottom element (`OrderBot α`), the infimum (greatest lower bound) of any element `a` of type `α` and the bottom element is always the bottom element. In other words, `⊥ ⊓ a = ⊥` for any `a` in `α`. This captures the intuitive idea that the greatest lower bound of any element and the least possible element is the least possible element itself.
More concisely: For any semilattice type `α` with a bottom element, the infimum of any element `a` is the bottom element itself: `∀α : Type, SemilatticeInf α OrderBot α → ∀a : α, ⊥ = ⊥⊓a`.
|
IsMin.eq_bot
theorem IsMin.eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsMin a → a = ⊥
The theorem `IsMin.eq_bot` states that for any type `α` endowed with a partial order and a least element, denoted by `⊥`, if an element `a` of `α` is minimal (in the sense that there is no element strictly less than `a`), then `a` must be equal to `⊥`. In other words, the least element `⊥` is the only minimal element in such a partially ordered set.
More concisely: In a partially ordered type with a least element, any minimal element equals the least element.
|
inf_eq_top_iff
theorem inf_eq_top_iff :
∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a b : α}, a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
The theorem `inf_eq_top_iff` states that for all types `α`, given a semilattice structure (which provides an infimum operation) and an order with top element on `α`, the infimum (greatest lower bound) of two elements `a` and `b` is the top element if and only if both `a` and `b` are the top element. In other words, the largest element that is less than or equal to both `a` and `b` is the top element of the order precisely when `a` and `b` are themselves the top element.
More concisely: For all types `α` with a semilattice and order structure having a top element, `top`, the infimum of `a` and `b` equals `top` if and only if `a` and `b` both equal `top`.
|
top_inf_eq
theorem top_inf_eq : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α), ⊤ ⊓ a = a
This theorem states that for any type `α` that is a semilattice under the operation of infimum (`⊓`) and has a defined top element (`⊤`), the infimum of the top element and any element `a` of the type is `a` itself. In more familiar mathematical terms, this says that in any partially ordered set which is a semilattice with greatest element, the greatest element 'meet' any element is that element itself. This reflects the intuitive idea that the intersection of any set with a universal set gives back the original set.
More concisely: In a semilattice with a top element, the infimum of the top element and any element is that element itself.
|
subsingleton_iff_bot_eq_top
theorem subsingleton_iff_bot_eq_top :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ ↔ Subsingleton α
This theorem states that for any type `α` with a partial order and a bounded order, the bottom element `⊥` is equal to the top element `⊤` if and only if `α` is a subsingleton. In the context of order theory, a subsingleton is a set with at most one element, so `α` being a subsingleton would mean it cannot have distinct `⊥` and `⊤`.
More concisely: For a type `α` equipped with a partial order and a bottom element `⊥`, `⊥` equals the top element `⊤` if and only if `α` is a subsingleton (i.e., has at most one element).
|
isMax_iff_eq_top
theorem isMax_iff_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsMax a ↔ a = ⊤ := by
sorry
This theorem, `isMax_iff_eq_top`, states that for any type `α` which has a partial ordering and a greatest element (`OrderTop`), an element `a` of `α` is maximal (as defined by `IsMax`) if and only if `a` equals the greatest element of `α` (`⊤`). In other words, the only maximal element in such a type is the greatest element.
More concisely: For any type `α` with a partial ordering and a greatest element `⊤`, an element `a` is maximal (in terms of the ordering) if and only if `a = ⊤`.
|
bot_sup_eq
theorem bot_sup_eq : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α), ⊥ ⊔ a = a
This theorem states that, for any type `α` that is both a semilattice with respect to the supremum operation and has a least element (`OrderBot α`), the supremum (denoted by `⊔`) of the least element (denoted by `⊥`) and any element `a` of type `α` is always `a`. In other words, in such a structure, taking the supremum of the least element and any other element always yields that other element.
More concisely: For any semilattice `α` with a least element, `⊔ ⊥ a = a`.
|
isMin_bot
theorem isMin_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α], IsMin ⊥
The theorem `isMin_bot` states that for any type `α` that has a pre-order (a binary relation that is reflexive and transitive) and a least element (defined by `OrderBot α`), the least element, denoted by `⊥`, is a minimal element. In other words, there is no other element in `α` that is strictly less than the least element. This property is characterized by `IsMin`, meaning that if any element `b` of `α` is less than or equal to `⊥`, then `⊥` is less than or equal to `b`.
More concisely: For any type `α` with a pre-order and a least element `⊥`, `⊥` is the unique minimal element, i.e., for all `b` in `α`, `⊥ ≤ b` implies `b ≤ ⊥`.
|
eq_bot_iff
theorem eq_bot_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a = ⊥ ↔ a ≤ ⊥
This theorem states that for any type `α`, given it has a `PartialOrder` and `OrderBot` structures, an element `a` of type `α` is equal to the bottom element (⊥) if and only if `a` is less than or equal to this bottom element. This applies to any type that has a notion of partial order and a defined bottom element.
More concisely: For any type `α` equipped with a `PartialOrder` and `OrderBot` structure, an element `a` is the bottom element if and only if `a ≤ ⊥`.
|
Mathlib.Order.BoundedOrder._auxLemma.1
theorem Mathlib.Order.BoundedOrder._auxLemma.1 :
∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α] {a : α}, (a ≤ ⊤) = True
This theorem, from the Mathlib library in the Order.BoundedOrder section, asserts that for any type `α` which is equipped with a "less than or equal to" (`LE`) operation and a designated "top" element (`OrderTop`), any element `a` of this type is less than or equal to the top element. Essentially, it says that the top element is the greatest element in `α`, and all other elements are less than or equal to it.
More concisely: For any type `α` with a "less than or equal to" (`LE`) relation and a top element (`OrderTop`), every element `a` in `α` satisfies `a ≤ OrderTop`.
|
ne_top_of_le_ne_top
theorem ne_top_of_le_ne_top :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, b ≠ ⊤ → a ≤ b → a ≠ ⊤
This theorem states that for any type `α`, given that `α` has a partial order and an order top (i.e., a greatest element), if we have two elements `a` and `b` of `α` such that `b` is not the greatest element (i.e., `b ≠ ⊤`) and `a` is less than or equal to `b` (i.e., `a ≤ b`), then `a` cannot be the greatest element either (i.e., `a ≠ ⊤`). In other words, if `a` is not greater than `b` and `b` is not the top element, then `a` cannot be the top element.
More concisely: If `α` is a type with a partial order and an order top, and `a` and `b` are elements of `α` with `a ≤ b` and `b ≠ ⊤`, then `a ≠ ⊤`.
|
bot_ne_top
theorem bot_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : Nontrivial α], ⊥ ≠ ⊤
This theorem, `bot_ne_top`, states that for any type `α` that is a `PartialOrder` and a `BoundedOrder` and is nontrivial (meaning there are at least two distinct elements in `α`), the bottom element `⊥` (the least element in the set) is not equal to the top element `⊤` (the greatest element in the set). In plain English, in any nontrivial partially ordered set that has both a smallest and a largest element, the smallest and largest elements are not the same.
More concisely: In any nontrivial partially ordered set with a least (bottom) and greatest (top) element, the least and greatest elements are distinct.
|
ne_top_of_lt
theorem ne_top_of_lt : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a ≠ ⊤
This theorem states that for any given type `α` that has a `Preorder` and `OrderTop` structure (meaning it can be ordered and has a "top" or greatest element), if `a` and `b` are elements of `α` such that `a` is strictly less than `b`, then `a` cannot be the top element of `α`. This is intuitive because if `a` were the top element, there could not exist another element `b` which is greater than `a`.
More concisely: For any type `α` with a `Preorder` and `OrderTop` structure, if `a` is strictly less than `b` in `α`, then `a` cannot be the top element of `α`.
|
eq_bot_mono
theorem eq_bot_mono : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, a ≤ b → b = ⊥ → a = ⊥
This theorem, `eq_bot_mono`, states that for any given type `α` which has a partial order and a least element (denoted by ⊥), if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, and `b` is the least element (⊥), then `a` must also be the least element (⊥). In other words, in a partially ordered set with a bottom element, if `a` is not greater than `b` and `b` is the least possible value, `a` must be that least value as well.
More concisely: In a partially ordered set with a bottom element, if an element is less than or equal to the bottom element, then it is the bottom element itself.
|
Mathlib.Order.BoundedOrder._auxLemma.7
theorem Mathlib.Order.BoundedOrder._auxLemma.7 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, (⊤ ≤ a) = (a = ⊤)
This theorem, `Mathlib.Order.BoundedOrder._auxLemma.7`, states that for any type `α` with a partial order and an order top (greatest element), and for any element `a` of this type, the condition of the greatest element being less than or equal to `a` is equivalent to `a` being the greatest element. In terms of mathematical notation, `⊤ ≤ a` is equivalent to `a = ⊤`.
More concisely: The greatest element `⊤` of a partially ordered type `α` is equal to any element `a` if and only if `⊤` is less than or equal to `a`.
|
bot_lt_iff_ne_bot
theorem bot_lt_iff_ne_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ < a ↔ a ≠ ⊥ := by
sorry
This theorem, named `bot_lt_iff_ne_bot`, states that for any type `α` with a partial order and a least element (`OrderBot α`), an element `a` of type `α` is greater than the least element (denoted by `⊥`) if and only if `a` is not equal to the least element. In more mathematical terms, for any partially ordered set with a least element, any element is greater than the least element if and only if it is not the least element itself.
More concisely: For any partially ordered type with a least element, an element is greater than the least element if and only if it is not equal to the least element.
|
not_lt_bot
theorem not_lt_bot : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, ¬a < ⊥
This theorem states that for any type `α` that has a `Preorder` and `OrderBot` structure, any element `a` of type `α` cannot be less than the bottom element, denoted by `⊥`. In other words, in any preordered set with a smallest element, no element is less than this smallest element.
More concisely: In any preordered type with a bottom element, no element is strictly less than the bottom element.
|
top_sup_eq
theorem top_sup_eq : ∀ {α : Type u} [inst : SemilatticeSup α] [inst_1 : OrderTop α] (a : α), ⊤ ⊔ a = ⊤
The theorem `top_sup_eq` states that for any type `α` that is both a semilattice under a supremum operation (`⊔`) and has a top element (`⊤`), the supremum of the top element and any element `a` of type `α` is always the top element. In other words, for any element `a` in such a structure, `⊤ ⊔ a = ⊤`. This theorem captures the property of the top element in a semilattice, which is that it is at least as great as every other element in the structure.
More concisely: For any semilattice `α` with top element `⊤`, `⊤ ⊔ a = ⊤` for all `a ∈ α`.
|
Mathlib.Order.BoundedOrder._auxLemma.31
theorem Mathlib.Order.BoundedOrder._auxLemma.31 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : Nontrivial α], (⊤ = ⊥) = False := by
sorry
This theorem states that for any type `α` that has a partial order, bounded order, and is nontrivial, the greatest element `⊤` (often read as 'top' and can be seen as the 'maximum') cannot be equal to the least element `⊥` (often read as 'bottom' and can be seen as the 'minimum'). This theorem essentially confirms that in a nontrivial, bounded, and partially ordered set, the maximum and minimum elements are distinct.
More concisely: In a nontrivial, bounded partially ordered type, the greatest and least elements are distinct.
|
Mathlib.Order.BoundedOrder._auxLemma.9
theorem Mathlib.Order.BoundedOrder._auxLemma.9 :
∀ {α : Type u} [inst : LE α] [inst_1 : OrderBot α] {a : α}, (⊥ ≤ a) = True
This theorem, named `Mathlib.Order.BoundedOrder._auxLemma.9`, states that for any type `α` equipped with a less-than-or-equal-to (`LE`) relation and a bottom element (`OrderBot`), for any element `a` of type `α`, the statement that the bottom element is less than or equal to `a` is always true. This means that in the given order, every element is greater than or equal to the bottom element.
More concisely: For any type `α` with a `LE` relation and a bottom element `OrderBot`, `OrderBot ≤ a` holds for all `a : α`.
|
eq_bot_or_bot_lt
theorem eq_bot_or_bot_lt : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] (a : α), a = ⊥ ∨ ⊥ < a := by
sorry
This theorem, `eq_bot_or_bot_lt`, states that for any value `a` of a type `α` that has a partial order and a least element (`⊥`), `a` is either equal to the least element (`⊥`) or is greater than the least element. In mathematical terms, for all `a` in a partially ordered set `α` with a smallest element, `a` is either equal to `⊥` or `a` is larger than `⊥`.
More concisely: For all partially ordered sets `α` with a smallest element `⊥`, every element `a` in `α` is either equal to `⊥` or strictly greater than `⊥`.
|
Mathlib.Order.BoundedOrder._auxLemma.30
theorem Mathlib.Order.BoundedOrder._auxLemma.30 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [inst_2 : Nontrivial α], (⊥ = ⊤) = False := by
sorry
This theorem, from the `Mathlib.Order.BoundedOrder` namespace, states that for any type `α` which is a partial order, a bounded order, and is nontrivial, the bottom element (denoted by `⊥`) and the top element (denoted by `⊤`) of this order are not equal. In other words, it asserts that in any nontrivial partially ordered set that is also a bounded order, the least element is not the same as the greatest element.
More concisely: In any nontrivial partially ordered set that is also a bounded order, the bottom and top elements are distinct.
|
top_unique
theorem top_unique : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ⊤ ≤ a → a = ⊤
This theorem, named `top_unique`, states that for any type `α` that has a partial order and a top element (`OrderTop`), if the top element is less than or equal to any element `a` of the type, then that element `a` must be the top element. Essentially, it means in the given order, there cannot be any element greater than the top element.
More concisely: If `α` is a type with a partial order and a top element `top`, then `top ≤ a` for all `a` in `α` implies `top = a`.
|