WithTop.some_le_some
theorem WithTop.some_le_some : ∀ {α : Type u_1} {a b : α} [inst : LE α], some a ≤ some b ↔ a ≤ b
This theorem, `WithTop.some_le_some`, states that for any type `α` and any two elements `a` and `b` of that type, with the condition that the type `α` has a less-than-or-equal-to (`LE`) relation, the relation 'less than or equal to' for the option type of `α` with an extra top element (`some a ≤ some b`) is equivalent to the relation 'less than or equal to' for the original type elements (`a ≤ b`).
More concisely: For any type `α` with a `LE` relation and elements `a` and `b`, `some a ≤ some b` if and only if `a ≤ b`.
|
WithTop.coe_lt_top
theorem WithTop.coe_lt_top : ∀ {α : Type u_1} [inst : LT α] (a : α), ↑a < ⊤
This theorem states that for any type `α` that has a less than (`LT`) relation and given any element `a` of type `α`, the coersion of `a` (`↑a`) is always less than positive infinity (`⊤`). In other words, for all possible types with a less than operation, any value from that type is less than infinity when considered in the extended number system (which includes positive infinity).
More concisely: For any type `α` with a `LT` relation, and for all `a : α`, `↑a < ⊤`.
|
Mathlib.Order.WithBot._auxLemma.3
theorem Mathlib.Order.WithBot._auxLemma.3 : ∀ {α : Type u_1} {a : α}, (↑a = ⊥) = False
This theorem states that for any type `α` and any instance `a` of that type, the notion that the bottom element (`⊥`) is equal to the lifted version of `a` (denoted as `↑a`) is always false. This is essentially asserting the uniqueness of the bottom element in the context of order theory.
More concisely: For any type `α` and any of its inhabitants `a`, `⊥ ≠ ↑a` in order theory.
|
WithTop.top_le_iff
theorem WithTop.top_le_iff : ∀ {α : Type u_1} [inst : LE α] {a : WithTop α}, ⊤ ≤ a ↔ a = ⊤
This theorem, `WithTop.top_le_iff`, states that for any type `α` that has a "less than or equal to" relation (`LE α`), and any element `a` of the type `WithTop α` (which is the type `α` with an additional top element `⊤`), the condition that `⊤` is less than or equal to `a` is equivalent to `a` being equal to `⊤`. This essentially means that `⊤` is the greatest element in the `WithTop α` type, since it is less than or equal to itself and no other element.
More concisely: In a type `α` equipped with a partial order `LE α`, the top element `⊤` of `WithTop α` is equal to every element `a` if and only if `⊤` is less than or equal to `a`.
|
Mathlib.Order.WithBot._auxLemma.9
theorem Mathlib.Order.WithBot._auxLemma.9 : ∀ {α : Type u_1} {a b : α} [inst : LE α], (↑a ≤ ↑b) = (a ≤ b)
This theorem, `Mathlib.Order.WithBot._auxLemma.9`, states that for any type `α` and any two elements `a` and `b` of this type—if this type has a less than or equal to (`≤`) comparison operation—then the assertion that `a` is less than or equal to `b` when both are coerced to a type with a bottom (using the ↑ operator) is equivalent to the assertion that `a` is less than or equal to `b` without any coercion.
More concisely: For any type `α` with a `≤` relation and any `a, b : α`, the coercion `↑a ≤ ↑b` is equivalent to `a ≤ b`.
|
Mathlib.Order.WithBot._auxLemma.48
theorem Mathlib.Order.WithBot._auxLemma.48 : ∀ {α : Type u_1} [inst : LT α] (a : α), (↑a < ⊤) = True
This theorem states that for any type `α` that has a less-than (`<`) relation, and for any element `a` of this type `α`, the statement that `a` is less than infinity (`⊤`) is always true. Put simply, for any given type with an order, every element of that type is less than infinity.
More concisely: For any type `α` with a total order and any `a` in `α`, `a` < ⊤ (where ⊤ is the greatest element in `α` representing infinity).
|
WithTop.top_ne_coe
theorem WithTop.top_ne_coe : ∀ {α : Type u_1} {a : α}, ⊤ ≠ ↑a
This theorem, `WithTop.top_ne_coe`, asserts that for any type `α` and any element `a` of that type, the element when cast to the extended type `WithTop α` (which is the original type `α` extended with a top element `⊤`) is never equal to the top element `⊤`. In other words, no regular element from the original type can be equal to the top element in the extended type when that element is cast to the extended type.
More concisely: For any type `α` and its element `a`, the coercion of `a` to `WithTop α` is never equal to the top element `⊤` in `WithTop α`.
|
Mathlib.Order.WithBot._auxLemma.47
theorem Mathlib.Order.WithBot._auxLemma.47 : ∀ {α : Type u_1} [inst : LT α] {a b : α}, (some a < some b) = (a < b) := by
sorry
This theorem states that for any type `α` with a less-than `<` relation, and for any two elements `a` and `b` of type `α`, the inequality `some a < some b` is equivalent to `a < b`. Here, `some` denotes the 'option' type constructor, i.e., `some a` is the option type that contains the value `a`. Essentially, this theorem confirms that option types preserve the order of the underlying type.
More concisely: For any type `α` with a total order `<`, and for all `a` and `b` in `α`, `some a < some b` if and only if `a < b`.
|
Monotone.withTop_map
theorem Monotone.withTop_map :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Monotone (WithTop.map f)
This theorem states that for any types α and β, both equipped with a preorder, and any function `f` from α to β, if `f` is a monotone function, then the function obtained by lifting `f` to operate on values in `WithTop α` and `WithTop β` (using the `WithTop.map` function) is also monotone. In other words, monotonicity is preserved when a function is lifted to operate on the "with top" extension of its argument and result types.
More concisely: For any monotone functions $f : \alpha \to \beta$ between preordered types $\alpha$ and $\beta$, the lifted function $f : \text{WithTop}\ \alpha \to \text{WithTop}\ \beta$ obtained using $\text{WithTop.map}$ is also monotone.
|
WithBot.bot_ne_coe
theorem WithBot.bot_ne_coe : ∀ {α : Type u_1} {a : α}, ⊥ ≠ ↑a
This theorem states that for any type `α` and any element `a` of type `α`, the bottom element (denoted by `⊥`) is not equal to the co-element of `a` (denoted by `↑a`). In other words, no element of any type can be equal to the bottom element in the type `WithBot α`, which includes all elements of `α` along with a lowest (or "bottom") element.
More concisely: For all types `α` and elements `a` of type `α`, `⊥ ≠ ↑a` in `WithBot α`.
|
WithTop.coe_ne_top
theorem WithTop.coe_ne_top : ∀ {α : Type u_1} {a : α}, ↑a ≠ ⊤
This theorem states that for any type `α` and any element `a` of that type, the embedding of `a` into the `WithTop α` type is not equal to `⊤` (`top`). In other words, no regular element from the original type `α` can be represented as the special `top` element in the `WithTop α` type after it's embedded. This is in the context of the `WithTop` type constructor, which adds a top element to any given type.
More concisely: For any type `α` and element `a` of `α`, the embedding of `a` into `WithTop α` is not equal to the top element `⊤` in `WithTop α`.
|
Mathlib.Order.WithBot._auxLemma.13
theorem Mathlib.Order.WithBot._auxLemma.13 : ∀ {α : Type u_1} {a b : α} [inst : LT α], (↑a < ↑b) = (a < b)
This theorem states that for any type `α` and any two elements `a` and `b` of that type, where `α` has a defined "less than" (`<`) relation, the comparison of the "coerced" (or "uplifted") values of `a` and `b` is equivalent to the comparison of `a` and `b` themselves. In other words, lifting `a` and `b` to an encompassing type with a bottom element (`WithBot α`) doesn't change the result of their comparison.
More concisely: For any type `α` with a defined `<` relation and any `a`, `b` in `α`, `a < b` if and only if `WithBot a < WithBot b` in `WithBot α`.
|
WithBot.coe_unbot
theorem WithBot.coe_unbot : ∀ {α : Type u_1} (x : WithBot α) (hx : x ≠ ⊥), ↑(x.unbot hx) = x
The theorem `WithBot.coe_unbot` states that for any type `α` and any element `x` of the type `WithBot α` (which is `α` extended with the `⊥` (bottom) element), if `x` is not the bottom element (i.e., `x ≠ ⊥`), then applying the function `WithBot.unbot` to `x` (which gives us the underlying `α` element), and then lifting it back to `WithBot α` (using the coercion function `↑`), equals to the original `x`. Essentially, this theorem asserts that the `WithBot.unbot` function correctly extracts the underlying value from a non-bottom element of `WithBot α`, and this value can be re-lifted to the original element.
More concisely: For any type `α` and `x` in `WithBot α`, if `x ≠ ⊥`, then `WithBot.unbot x = x.up`.
|
StrictMono.withBot_map
theorem StrictMono.withBot_map :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → StrictMono (WithBot.map f)
This theorem, named `StrictMono.withBot_map`, states that given two types `α` and `β` each with a preorder relation, and a function `f` from `α` to `β`, if `f` is strictly monotone (meaning that for all `a` and `b` of type `α`, if `a` is less than `b`, then `f(a)` is less than `f(b)`), then the function resulting from lifting `f` to act on the type `WithBot α` (the type `α` augmented with a bottom element) and map to `WithBot β` is also strictly monotone.
More concisely: If `f` is a strictly monotone function between preordered types `α` and `β`, then the lifted function `WithBot f` from `WithBot α` to `WithBot β`, where `WithBot` denotes the addition of a bottom element, is also strictly monotone.
|
WithBot.some_eq_coe
theorem WithBot.some_eq_coe : ∀ {α : Type u_1} (a : α), some a = ↑a
This theorem, `WithBot.some_eq_coe`, states that for any type `α` and for any instance `a` of that type, wrapping `a` with `some` operator is equivalent to coercing `a` to its `WithBot` form. In simpler terms, this theorem asserts an equivalence between the option-wrapped form and the subtype-wrapped form of any given instance of a type.
More concisely: For any type `α` and instance `a` of it, `some (someDem cry a) = coe (withBot a)`, where `someDem` is the default `some` constructor and `withBot` is the `WithBot` subtype constructor.
|
WithBot.coe_le_coe
theorem WithBot.coe_le_coe : ∀ {α : Type u_1} {a b : α} [inst : LE α], ↑a ≤ ↑b ↔ a ≤ b
This theorem, `WithBot.coe_le_coe`, states that for any type `α` and any two elements `a` and `b` of this type that have a less-than-or-equal-to (`≤`) relation defined on them, the less-than-or-equal-to relation between their coe (or coercion) holds if and only if the less-than-or-equal-to relation between `a` and `b` holds. In other words, the order is preserved when we move from the original elements to their coerced versions.
More concisely: For any type `α` with a `≤` relation and elements `a` and `b` of `α`, if `a ≤ b`, then their coerced versions have the same relationship: `coe a ≤ coe b` (or `coe b ≥ coe a`).
|
WithTop.strictMono_iff
theorem WithTop.strictMono_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithTop α → β},
StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ↑x < f ⊤
This theorem states that for any types `α` and `β` that have preorder structures and any function `f` from `WithTop α` to `β`, `f` is strictly monotone if and only if the function obtained from `f` by restricting its domain to the non-top elements of `WithTop α` is strictly monotone and, for every element `x` of `α`, `f` applied to `x` (lifted to `WithTop α`) is strictly less than `f` applied to the top element of `WithTop α`. In other words, `f` is strictly increasing, and the top element of `WithTop α` is mapped to a value strictly greater than any non-top element.
More concisely: For functions between preordered types `α` and `β`, `f` is strictly monotone if and only if its restriction to non-top elements is strictly monotone and for all `x` in `α`, `f` maps `x` to a strictly lesser value than `f` applied to the top element of `WithTop α`.
|
WithBot.none_lt_some
theorem WithBot.none_lt_some : ∀ {α : Type u_1} [inst : LT α] (a : α), none < ↑a
This theorem states that for any type `α` which has a less-than operation (`LT α`), any value `a` of type `α` satisfies the inequality that `none` is less than `a`. Here, `none` refers to the bottom element of the type `WithBot α` (which adds a bottom element to `α`), and `↑a` is the notation for lifting `a` into the `WithBot α` type. So, in other words, the bottom element of `WithBot α` is less than any other element of this type.
More concisely: For any type `α` with a less-than relation and any element `a` of type `α`, `none` (the bottom element of `WithBot α`) is less than `a` in `WithBot α`.
|
WithBot.coe_eq_coe
theorem WithBot.coe_eq_coe : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
This theorem, `WithBot.coe_eq_coe`, states that for any type `α` and for any two elements `a` and `b` of type `α`, the condition that the coercion of `a` to the `WithBot` type equals the coercion of `b` to the `WithBot` type is equivalent to `a` being equal to `b`. In other words, the coercions of two elements to the `WithBot` type are equal if and only if the elements themselves are equal.
More concisely: For any type `α` and elements `a` and `b` of type `α`, `WithBot.coe a = WithBot.coe b` if and only if `a = b`.
|
WithBot.unbot'_le_iff
theorem WithBot.unbot'_le_iff :
∀ {α : Type u_1} [inst : LE α] {a : WithBot α} {b c : α}, (a = ⊥ → b ≤ c) → (WithBot.unbot' b a ≤ c ↔ a ≤ ↑c) := by
sorry
This theorem states that for any type `α` that has a less-than-or-equal-to (`≤`) relation, and for any elements `a` of the type `WithBot α` and `b` and `c` of type `α`, if `b` is less than or equal to `c` when `a` is bottom (`⊥`), then `WithBot.unbot' b a` being less than or equal to `c` is equivalent to `a` being less than or equal to the co-domain of `c`. In other words, it shows the equivalence of these two conditions under the provided assumptions.
More concisely: For any type `α` with a `≤` relation, and for any `a ∈ WithBot α`, `b`, `c ∈ α`, if `a = ⊥` implies `b ≤ c` then `WithBot.unbot' b a ≤ c` if and only if `a ≤ co-domain of c`.
|
Mathlib.Order.WithBot._auxLemma.1
theorem Mathlib.Order.WithBot._auxLemma.1 : ∀ {α : Type u_1} {a b : α}, (↑a = ↑b) = (a = b)
This theorem, named `_auxLemma.1` from the `Mathlib.Order.WithBot` namespace in Lean, states that for any type `α` and any two elements `a` and `b` of type `α`, the statement that the type-coerced `a` is equal to the type-coerced `b` is equivalent to the statement that `a` is equal to `b`. In other words, coercion does not change the equality relation between `a` and `b`.
More concisely: For any type `α` and elements `a`, `b` of type `α` in Lean, the coerced elements `α to α a` and `α to α b` are equal if and only if `a` and `b` are equal.
|
WithBot.le_bot_iff
theorem WithBot.le_bot_iff : ∀ {α : Type u_1} [inst : LE α] {a : WithBot α}, a ≤ ⊥ ↔ a = ⊥
This theorem states that for any type `α` that has a `less than or equal to` structure (`LE α`), and for any value `a` of the enhanced type `WithBot α` (which is `α` plus an extra bottom element), the value `a` is less than or equal to this bottom element if and only if `a` is the bottom element itself. In other words, in this context, only the bottom element (designated as `⊥`) is less than or equal to itself.
More concisely: For any type `α` with a `less than or equal to` structure and any value `a` in the enhanced type `WithBot α`, `a ≤ ⊥` if and only if `a = ⊥`.
|
WithTop.some_lt_some
theorem WithTop.some_lt_some : ∀ {α : Type u_1} [inst : LT α] {a b : α}, some a < some b ↔ a < b
This theorem states that for all types `α` equiped with a less-than ordering (denoted by `LT α`), given any two elements `a` and `b` from `α`, the wrapped value `some a` is less than `some b` within the `WithTop` type if and only if `a` is less than `b` in the original type `α`. The `WithTop` type is a type construction that adds an element "top" to a given type, usually representing an infinity or a maximum element.
More concisely: For all types `α` with a less-than ordering and for all `a` and `b` in `α`, `some a < some b` in the `WithTop α` type if and only if `a < b` in `α`.
|
WithBot.unbot'_coe
theorem WithBot.unbot'_coe : ∀ {α : Type u_5} (d x : α), WithBot.unbot' d ↑x = x
The theorem `WithBot.unbot'_coe` states that for any type `α` and any two elements `d` and `x` of that type, when `x` is coerced into `WithBot α` type and then the `WithBot.unbot'` function is applied with `d` as default value, we get back original `x`. This essentially asserts that the `WithBot.unbot'` function is a kind of inverse operation to coercion into `WithBot α` type, at least when the original value was from `α` and not `bot`.
More concisely: For any type `α` and elements `d : α` and `x : α`, `WithBot.unbot' d x = x`.
|
Mathlib.Order.WithBot._auxLemma.33
theorem Mathlib.Order.WithBot._auxLemma.33 : ∀ {α : Type u_1} {a b : α} [inst : LE α], (↑a ≤ ↑b) = (a ≤ b)
This theorem states that for any type `α` and any two elements `a` and `b` of this type, provided that `α` has a less-than-or-equal-to (`≤`) operation, the statement that `a` is less than or equal to `b` when both are lifted to the type WithBot α (represented as `↑a ≤ ↑b`), is equivalent to the statement that `a` is less than or equal to `b` in the original type `α`. In other words, the less-than-or-equal-to relation is preserved when elements are lifted to the WithBot type.
More concisely: For any type `α` equipped with a `≤` relation and any `a, b ∈ α`, `a ≤ b` is equivalent to `↑a ≤ ↑b` in the type `WithBot α`, where `↑` denotes the lifting function.
|
Mathlib.Order.WithBot._auxLemma.46
theorem Mathlib.Order.WithBot._auxLemma.46 : ∀ {α : Type u_1} [inst : LT α] {a b : α}, (↑a < ↑b) = (a < b)
This theorem states that for any type `α` with a less than (`<`) operation, and any two elements `a` and `b` of this type, the inequality `↑a < ↑b` is equivalent to `a < b`. Here, `↑a` and `↑b` denote the lift of `a` and `b` to an extended type that includes a "bottom" element (represented as `WithBot α`). Essentially, this theorem ensures that the inequality relationship between `a` and `b` is preserved when they are lifted to the `WithBot α` type.
More concisely: For any type `α` with a total order and any elements `a` and `b` of `α`, `a < b` is equivalent to `↑a < ↑b` in the type `WithBot α`, where `↑` denotes lifting to `WithBot α`.
|
WithBot.bot_lt_iff_ne_bot
theorem WithBot.bot_lt_iff_ne_bot : ∀ {α : Type u_1} [inst : LT α] {x : WithBot α}, ⊥ < x ↔ x ≠ ⊥
This theorem is a version of the `bot_lt_iff_ne_bot` for `WithBot`, which is a type that extends another type by adding a "bottom" element. The theorem states that for all types `α`, endowed with a less than (`LT`) operation, and for all values `x` of type `WithBot α`, `⊥` (the bottom element) is less than `x` if and only if `x` is not equal to `⊥`. The theorem does not require `α` to have a `PartialOrder` structure, only a `LT` (less than) operation.
More concisely: For any type endowed with a less than operation, the bottom element is less than any non-bottom value in the type with bottom element.
|
WithTop.coe_untop
theorem WithTop.coe_untop : ∀ {α : Type u_1} (x : WithTop α) (hx : x ≠ ⊤), ↑(x.untop hx) = x
The theorem `WithTop.coe_untop` states that for any type `α` and for any element `x` of the type `WithTop α` which is not equal to `⊤` (Top), the result of applying the `untop` function to `x` and then embedding it back into the `WithTop α` type using the coercion function `↑` (up arrow), is equal to the original element `x` itself. In other words, the operation of `untop` followed by re-embedding is an identity operation for any element other than `⊤` in `WithTop α`.
More concisely: For all types `α` and elements `x` in `WithTop α` distinct from `⊤`, the operation of `untop` followed by coercion `↑` is the identity function on `x`, i.e., `untop ↑x = x`.
|
WithBot.some_lt_some
theorem WithBot.some_lt_some : ∀ {α : Type u_1} {a b : α} [inst : LT α], some a < some b ↔ a < b
This theorem, `WithBot.some_lt_some`, states that for any type `α` and any two elements `a` and `b` of that type, given a less-than (`LT`) ordering on `α`, the comparison `some a < some b` is equivalent to `a < b`. In other words, the ordering on the optional version of the type (`WithBot α`) aligns with the original ordering on the type itself.
More concisely: For any type `α` and its optional version `WithBot α`, and for all `a` and `b` in `α`, `some a < some b` if and only if `a < b` holds in the base type.
|
WithTop.forall
theorem WithTop.forall : ∀ {α : Type u_1} {p : WithTop α → Prop}, (∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x := by
sorry
The theorem `WithTop.forall` states that for any type `α` and any property `p` defined over the type `WithTop α` (which is the type `α` augmented with an additional element `⊤`), the property `p` holds for all elements of `WithTop α` if and only if `p` holds for the `⊤` element and `p` holds for every element of `α` when lifted to the `WithTop α` type. The lifting is denoted by `p ↑x` and it simply means applying the property `p` to the element `x` of `α` considered as an element of `WithTop α`.
More concisely: For any type `α` and property `p` on `α`, `WithTop.forall` asserts that an element `x` in `WithTop α` has property `p` if and only if the top element `⊤` has property `p` and every element `x` in `α` does when lifted to `WithTop α`.
|
WithTop.coe_eq_coe
theorem WithTop.coe_eq_coe : ∀ {α : Type u_1} {a b : α}, ↑a = ↑b ↔ a = b
This theorem states that for any type `α` and any two values `a` and `b` of type `α`, the equality of their coe (ie., their coerced/converted values) in the WithTop type is equivalent to their equality in the original type. In other words, `a` and `b` are equal if and only if their coerced versions are equal. This theorem provides the basis for doing equality checks on possibly infinite objects (i.e., values of the `WithTop α` type).
More concisely: For any type `α` and values `a` and `b` of type `α`, the equality `a = b` holds if and only if the equality of their coerced values `coe a = coe b` in `WithTop α` holds.
|
WithBot.strictMono_iff
theorem WithBot.strictMono_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithBot α → β},
StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ⊥ < f ↑x
The theorem `WithBot.strictMono_iff` states that for any two types `α` and `β` that have a preorder relation, a function `f` from `WithBot α` to `β` is strictly monotone if and only if the following two conditions hold: (1) the function `f` applied to any `a` in the domain, where `a` is lifted into `WithBot α`, is strictly monotone, and (2) for any `x` in `α`, the value of `f` at `⊥` (the bottom element in `WithBot α`) is less than the value of `f` at the lifted `x`. Essentially, strict monotonicity of `f` in the extended domain `WithBot α` is characterized by its strict monotonicity in the original domain `α` and its behavior at `⊥`.
More concisely: A function from types equipped with bottom elements to another type is strictly monotone if and only if its restriction to the original types is strictly monotone and it maps the bottom element to a value less than any other image under the function.
|
WithTop.coe_le_coe
theorem WithTop.coe_le_coe : ∀ {α : Type u_1} {a b : α} [inst : LE α], ↑a ≤ ↑b ↔ a ≤ b
This theorem, `WithTop.coe_le_coe`, states that for any type `α` and any two instances `a` and `b` of that type, given that `α` has a less-than-or-equal-to (`≤`) relation defined on it, the less-than-or-equal-to relation of the lifted values (`↑a` and `↑b`) in the extended type `WithTop α` (i.e., `α` with an added element denoted as 'top') mirrors the less-than-or-equal-to relation of `a` and `b` in the original type `α`. In other words, `a` is less than or equal to `b` in type `α` if and only if the lift of `a` is less than or equal to the lift of `b` in `WithTop α`.
More concisely: For any type `α` with a `≤` relation and any `a` and `b` in `α`, `↑a ≤ ↑b` in `WithTop α` if and only if `a ≤ b` in `α`.
|
Mathlib.Order.WithBot._auxLemma.2
theorem Mathlib.Order.WithBot._auxLemma.2 : ∀ {α : Type u_1} {a : α}, (⊥ = ↑a) = False
This theorem from the Mathlib Order WithBot module states that, for any type `α` and any element `a` of type `α`, the equality between the bottom element (`⊥`) and the lifted version of `a` (`↑a`) is always false. In other words, no matter what specific type and element we are working with, the bottom element of the order can never be considered as the lift of any element from the underlying type.
More concisely: For all types `α` and elements `a` of type `α`, `⊥ ≠ ↑a`.
|
Monotone.withBot_map
theorem Monotone.withBot_map :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
Monotone f → Monotone (WithBot.map f)
The theorem `Monotone.withBot_map` states that for all types `α` and `β` that have a predefined order (`Preorder`), if we have a function `f` from `α` to `β` that is monotone (meaning that if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`), then the function `WithBot.map f` is also monotone. Here, `WithBot.map f` is a function that lifts `f` from `α → β` to `WithBot α → WithBot β`, where `WithBot α` is the type `α` extended with an element `bot` that is less than all elements of `α`.
More concisely: If `f : α → β` is a monotone function between preordered types `α` and `β`, then the lifted function `WithBot.map f : WithBot α → WithBot β` is also monotone.
|
Mathlib.Order.WithBot._auxLemma.24
theorem Mathlib.Order.WithBot._auxLemma.24 : ∀ {α : Type u_1} {a b : α}, (↑a = ↑b) = (a = b)
This theorem, `Mathlib.Order.WithBot._auxLemma.24`, states that for any type `α` and any two elements `a` and `b` of that type, the equality of the 'lifted' versions of `a` and `b` (denoted as `↑a` and `↑b`) is equivalent to the equality of `a` and `b` themselves. In the context of order theory, 'lifting' often means embedding a set into a larger set where the original set elements maintain their order relation. Here, it implies that the equality of elements holds true even after they have been 'lifted' (or embedded) into some larger structure, such as a set with added bottom element (which is what `WithBot` refers to).
More concisely: For any type `α` and its elements `a` and `b`, `↑a = ↑b` if and only if `a = b`.
|
WithTop.lt_top_iff_ne_top
theorem WithTop.lt_top_iff_ne_top : ∀ {α : Type u_1} [inst : LT α] {x : WithTop α}, x < ⊤ ↔ x ≠ ⊤
This theorem, `WithTop.lt_top_iff_ne_top`, states that for any type `α` equipped with a less than (`LT`) relation, and for any value `x` of the type `WithTop α` (that is, `α` extended with a top element), `x` is less than the top element if and only if `x` is not equal to the top element. This theorem doesn't require `α` to have a partial order structure, only a less than relation.
More concisely: For any type `α` with a less than relation `LT`, and for any `x` in `WithTop α`, `x` is less than the top element if and only if `x` is not equal to the top element.
|
StrictMono.withTop_map
theorem StrictMono.withTop_map :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
StrictMono f → StrictMono (WithTop.map f)
This theorem, denoted as `StrictMono.withTop_map`, states that for any types `α` and `β` with preorder relations, if a function `f` from `α` to `β` is strictly monotone (i.e., for all `a` and `b` in `α`, if `a` is less than `b`, then `f(a)` is less than `f(b)`), then the function obtained by lifting `f` to operate on the `WithTop` versions of `α` and `β` (i.e., `α` and `β` extended with an element "top" that is greater than all other elements) is also strictly monotone. In other words, strict monotonicity is preserved when the function `f` is lifted to operate on the `WithTop` extensions of its original domains.
More concisely: If `f` is a strictly monotone function between preordered types `α` and `β`, then the extended function `f` on their `WithTop` versions is also strictly monotone.
|
WithBot.not_coe_le_bot
theorem WithBot.not_coe_le_bot : ∀ {α : Type u_1} [inst : LE α] (a : α), ¬↑a ≤ ⊥
This theorem states that for any type `α` that has a less than or equal to (`LE`) operation, and any instance `a` of that type, the coerced value of `a` (`↑a`) is not less than or equal to the bottom element (`⊥`). In other words, no element in the `WithBot α` extension of `α` is less than or equal to the bottom element. This is essentially a statement about the order properties of the "with bottom" extension of a pre-existing ordered type.
More concisely: For any type `α` with a `LE` relation and any `a : α`, the coerced value `↑a` does not `LE` the bottom element `⊥` in the `WithBot α` extension.
|
WithBot.bot_lt_coe
theorem WithBot.bot_lt_coe : ∀ {α : Type u_1} [inst : LT α] (a : α), ⊥ < ↑a
This theorem states that, for any type `α` that has a less-than (`LT`) operation, and for any element `a` of type `α`, the bottom element (denoted as `⊥`) is less than the `a` element when `a` is lifted (coerced) into the "WithBot α" type. This is a formalization of the intuitive idea that the bottom element is less than any other element in the order.
More concisely: For any type `α` with a `LT` operation and any `a : α`, `⊥ : WithBot α` holds `LT ⊥ a`.
|
WithBot.some_le_some
theorem WithBot.some_le_some : ∀ {α : Type u_1} {a b : α} [inst : LE α], some a ≤ some b ↔ a ≤ b
This theorem, "WithBot.some_le_some", states that for any type 'α' and any two elements 'a' and 'b' of that type, given that the type 'α' has a less than or equal to (≤) relation defined, 'some a' is less than or equal to 'some b' if and only if 'a' is less than or equal to 'b'. "WithBot" is a type constructor that adds a bottom element to a given type, and "some" is a constructor that embeds elements of the original type into the WithBot type. The theorem essentially establishes that the order relation is preserved under this embedding.
More concisely: For any type with a ≤ relation, the embedding of elements into the type WithBot with bottom element preserves the order relation: i.e., a ≤ b if and only if some a ≤ some b.
|
WithBot.not_lt_none
theorem WithBot.not_lt_none : ∀ {α : Type u_1} [inst : LT α] (a : WithBot α), ¬a < none
This theorem, `WithBot.not_lt_none`, states that for any type `α` that has a less-than order `LT`, and for any element `a` of the type `WithBot α` (which is `α` with a bottom element `⊥` added), `a` is not less than `none` (which corresponds to `⊥`). In simpler terms, no element of `WithBot α` is less than the bottom element `⊥`.
More concisely: For any type `α` with a less-than order `LT`, and for any `a` in `WithBot α`, we have `a ≻ ⊥` (`a` is not less than the bottom element `⊥`).
|
WithTop.not_top_le_coe
theorem WithTop.not_top_le_coe : ∀ {α : Type u_1} [inst : LE α] (a : α), ¬⊤ ≤ ↑a
This theorem states that for any type `α` that has a less than or equal to (`≤`) operation, and any instance `a` of that type, the "top" element (represented by `⊤`) is not less than or equal to the coerced version of `a` (represented by `↑a`). In other words, there's no instance of a type that's greater than or equal to the top element in the "WithTop" type augmentation of `α`. This is somewhat analogous to saying that there's no real number greater than or equal to infinity.
More concisely: For any type `α` with a `≤` relation and any `a : α`, the top element `⊤` of `WithTop α` is not less than or equal to the coerced `↑a`. In symbols: `∀ (α : Type) [DecidableRelation ≤ α], ∀ a : α, ⊤ : WithTop α <≤ ↑a`.
|
WithBot.coe_lt_coe
theorem WithBot.coe_lt_coe : ∀ {α : Type u_1} {a b : α} [inst : LT α], ↑a < ↑b ↔ a < b
This theorem, `WithBot.coe_lt_coe`, states that for any type `α` and any two elements `a` and `b` of that type, where the type has a less-than (`LT`) relation defined on it, the proposition "`a` is less than `b`" is equivalent to the proposition "the coerced value of `a` is less than the coerced value of `b`". Here, the coercion refers to the process of embedding `α` into the type `WithBot α`, which adjoins an additional 'bottom' element to `α`.
More concisely: For any type `α` with a less-than relation and any `a` and `b` in `α`, `a < b` if and only if `coe (WithBot.coerce a) < coe (WithBot.coerce b)` in the type `WithBot α`.
|
WithBot.coe_ne_bot
theorem WithBot.coe_ne_bot : ∀ {α : Type u_1} {a : α}, ↑a ≠ ⊥
This theorem states that for any given type `α` and any element `a` of that type, the coercion of `a` to the `WithBot α` type (which is the type `α` extended with a bottom element `⊥`) is not equal to the bottom element `⊥`. In other words, any concrete element of the original type, when lifted to the extended type with a bottom element, does not become the bottom element.
More concisely: For any type `α` and its element `a`, the coercion of `a` to `WithBot α` is not equal to the bottom element `⊥` of `WithBot α`.
|
Mathlib.Order.WithBot._auxLemma.15
theorem Mathlib.Order.WithBot._auxLemma.15 : ∀ {α : Type u_1} [inst : LT α] (a : α), (⊥ < ↑a) = True
This theorem, named `Mathlib.Order.WithBot._auxLemma.15`, states that for any type `α` that has a less-than relation (`LT`), and for any element `a` of this type, the statement "the bottom element is less than the co-domain of `a`" always holds true. Here, `⊥` denotes the bottom element, and `↑a` refers to the co-domain of `a`. The theorem essentially establishes that any value in the type `α` is always greater than the bottom element, within the context of ordered types.
More concisely: For any type `α` with a less-than relation and any element `a` in `α`, the bottom element `⊥` is less than the co-domain `↑a` of `a`. (Or equivalently, every element `a` in `α` is greater than the bottom element `⊥` in the order `LT`.)
|
Mathlib.Order.WithBot._auxLemma.26
theorem Mathlib.Order.WithBot._auxLemma.26 : ∀ {α : Type u_1} {a : α}, (↑a = ⊤) = False
This theorem, `Mathlib.Order.WithBot._auxLemma.26`, states that for any type `α` and any element `a` of that type, the proposition that this element `a` (when coerced) equals to the top element `⊤` (also known as "infinity" in the context of orders), is always false. In other words, any specific element of a type cannot be equal to the top element when we are working in the lattice of with-bottom elements.
More concisely: For any type `α` and its element `a`, `a` does not equal the top element `⊤` in the lattice of with-bottom elements.
|
WithBot.coe_le_iff
theorem WithBot.coe_le_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α}, ↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b := by
sorry
This theorem, `WithBot.coe_le_iff`, states that for any type `α` with a less than or equal to (`≤`) relation, and any element `a` of type `α`, and any element `x` of the type `WithBot α` (which is `α` with a bottom element), the coerced element `a` is less than or equal to `x` if and only if there exists an element `b` such that `x` equals the coerced `b` and `a` is less than or equal to `b`. In other words, an element of `α` is less than or equal to an element of `WithBot α` if and only if it is less than or equal to some actual element of `α` that `x` represents.
More concisely: For any type `α` with a total order and any `α` elements `a` and `x` where `x` is of type `WithBot α`, `a ≤ x` if and only if there exists `b : α` such that `x = WithBot.coe b` and `a ≤ b`.
|
WithTop.coe_lt_coe
theorem WithTop.coe_lt_coe : ∀ {α : Type u_1} [inst : LT α] {a b : α}, ↑a < ↑b ↔ a < b
This theorem, `WithTop.coe_lt_coe`, is about type lifting and comparison in a partially ordered set. It states that for all types `α` with a less-than order (`LT`) and for every pair of elements `a` and `b` from `α`, the statement "coerced `a` is less than coerced `b`" holds if and only if " `a` is less than `b`". Here, coercion `↑` is used for embedding `α` into an extended type that includes a top element, and the comparison `<` is with respect to the order on `α`.
More concisely: For any type `α` with a less-than order and for all `a` and `b` in `α`, `↑a < ↑b` if and only if `a < b`.
|