WithTop.preimage_coe_Iio_top
theorem WithTop.preimage_coe_Iio_top : ∀ {α : Type u_1} [inst : Preorder α], WithTop.some ⁻¹' Set.Iio ⊤ = Set.univ := by
sorry
This theorem states that for any type `α` endowed with a preorder structure, the preimage of the left-infinite right-open interval `Set.Iio ⊤` under the canonical map `WithTop.some : α → WithTop α` is the universal set `Set.univ`. In other words, every element of `α` is mapped to a value less than `⊤` (top) in the `WithTop α` structure. It essentially shows that all elements of the original set `α` are considered less than infinity (`⊤`) in the extended set `WithTop α`.
More concisely: For any type `α` with a preorder structure, the image of `α` under the canonical map to `WithTop α` is the set of elements less than the top element in `WithTop α`, i.e., `WithTop.some'' Set.univ = Set.Iio ⊤`.
|
WithBot.preimage_coe_Iic
theorem WithBot.preimage_coe_Iic :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Iic ↑a = Set.Iic a
This theorem states that for any type `α` with a preorder, and for any `a` in `α`, the preimage of the interval set `Set.Iic ↑a` under the function `WithBot.some` is equal to the interval `Set.Iic a`. In simpler terms, it means that when we map elements from type `α` to the type `WithBot α` and then take elements that are less than or equal to `a` (in `WithBot α`), it's equivalent to directly taking elements that are less than or equal to `a` in type `α`. Here, `WithBot.some` is a function that embeds type `α` into `WithBot α` and `Set.Iic a` is the set of all elements less than or equal to `a`.
More concisely: For any preordered type `α` and element `a` in `α`, the preimage of the interval `[a, ∞)` under the embedding `WithBot.some` is equal to the interval `[a, ∞)` in `α`.
|
WithTop.preimage_coe_Ici
theorem WithTop.preimage_coe_Ici :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ici ↑a = Set.Ici a
This theorem states that for any type `α` equipped with a preorder structure and for any element `a` of type `α`, the preimage of the left-closed right-infinite interval starting at the element `a` under the canonical map from `α` into `WithTop α` is equal to the left-closed right-infinite interval starting at `a`. In other words, for all elements from `a` and above (inclusive), their images under the embedding into `WithTop α` are precisely the elements from `a` and above in the `WithTop α` set.
More concisely: For any preordered type `α` and element `a` in `α`, the image of the left-closed right-infinite interval [a, ∞) under the embedding of `α` into `WithTop α` is equal to the left-closed right-infinite interval [a, ∞) in `WithTop α`.
|
WithBot.preimage_coe_Iio
theorem WithBot.preimage_coe_Iio :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Iio ↑a = Set.Iio a
This theorem states that for any type `α` that has a preorder structure (i.e., a set in which an order relation is defined), and for any element `a` of this type, the preimage of the set of elements less than `a` under the function that maps each element of `α` to the corresponding element in `WithBot α` (i.e., `α` supplemented with a least element) is exactly the set of elements less than `a`. In other words, applying the `WithBot.some` function to the set of elements less than `a` in α doesn't change the set.
More concisely: For any preordered type `α` and element `a` in `α`, the set of elements less than `a` is equal to the preimage of `{x : WithBot α | x < a}` under the natural inclusion function from `α` to `WithBot α`.
|
WithBot.preimage_coe_Ioi
theorem WithBot.preimage_coe_Ioi :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
This theorem states that for any type `α` that has a preorder structure and any element `a` of that type, the preimage of the set of elements greater than `a` (not inclusive) under the canonical map from `α` to `WithBot α` is equal to the set of elements greater than `a` in `α`. In other words, applying the canonical mapping to the set of elements greater than `a` in `α` doesn't change the set; it remains the set of elements greater than `a`.
More concisely: For any preordered type `α` and element `a` in `α`, the image of the set of elements strictly greater than `a` under the canonical map from `α` to `WithBot α` is equal to the set of elements strictly greater than `a` in `α`.
|
WithBot.range_coe
theorem WithBot.range_coe : ∀ {α : Type u_1} [inst : Preorder α], Set.range WithBot.some = Set.Ioi ⊥
The theorem `WithBot.range_coe` states that for any type `α`, given an instance of `Preorder` for `α`, the range of the canonical function `WithBot.some` (which maps `α` into `WithBot α`) is equal to the set of elements of `α` that are greater than the bottom element (`⊥`). In other words, every element in the range of `WithBot.some` is strictly greater than the bottom element (`⊥`), which makes it equivalent to the set defined by the left-open right-infinite interval (`Set.Ioi ⊥`).
More concisely: For any type `α` with a preorder structure, the range of `WithBot.some : α → WithBot α` consists of elements strictly greater than the bottom element (⊥), equivalent to `Set.Ioi ⊥`.
|
WithBot.preimage_coe_Ioi_bot
theorem WithBot.preimage_coe_Ioi_bot : ∀ {α : Type u_1} [inst : Preorder α], WithBot.some ⁻¹' Set.Ioi ⊥ = Set.univ := by
sorry
The theorem `WithBot.preimage_coe_Ioi_bot` states that for any type `α` with a preorder structure, the preimage of the set of elements strictly greater than the bottom element (⊥) under the canonical map from `α` to `WithBot α` is the universal set. In other words, for every element in `α`, there is an element in `WithBot α` that is strictly greater than ⊥ and maps to it. This is because `WithBot.some` function (canonical map) always lifts an element from `α` to an element in `WithBot α` that is greater than ⊥. Hence, all elements of `α` are included in this preimage, making it equal to the universal set.
More concisely: For any preordered type `α`, the preimage of the set of elements strictly greater than its bottom element under the canonical map from `α` to `WithBot α` equals the universal set.
|
WithTop.range_coe
theorem WithTop.range_coe : ∀ {α : Type u_1} [inst : Preorder α], Set.range WithTop.some = Set.Iio ⊤
This theorem states that for any type `α` that has a preorder relation, the set of all values that can be produced by the `WithTop.some` function (which maps each element of `α` to an element of the type `WithTop α`, essentially adding a "top" or maximal element to `α`) is exactly the same as the set of all values in `WithTop α` that are strictly less than the top element. In other words, every element in the type `WithTop α` except for the top element can be reached by applying `WithTop.some` to some element of `α`.
More concisely: For any preordered type `α`, the image of `α` under `WithTop.some` is equal to the set of strictly smaller elements in `WithTop α`.
|
WithTop.preimage_coe_Ioi
theorem WithTop.preimage_coe_Ioi :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
The theorem `WithTop.preimage_coe_Ioi` states that for any type `α` equipped with a preorder and any element `a` of `α`, the preimage of the set of elements greater than the element `a` under the canonical embedding of `α` into `WithTop α` is exactly the set of elements greater than `a` in `α`. In other words, the measure of elements greater than `a` in `WithTop α` is equivalent to the measure of elements greater than `a` in `α`.
More concisely: For any preordered type `α` and element `a` in `α`, the preimage of the set of elements greater than `a` under the canonical embedding of `α` into `WithTop α` equals the set of elements in `α` greater than `a`.
|
WithTop.preimage_coe_Iio
theorem WithTop.preimage_coe_Iio :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Iio ↑a = Set.Iio a
This theorem states that for any type `α`, given a preorder on `α` and a value `a` of type `α`, the preimage under the function `WithTop.some`, which maps from `α` into `WithTop α`, of the set of all elements in `WithTop α` less than `a` (i.e., `Set.Iio ↑a`) is equal to the set of all elements in `α` less than `a` (i.e., `Set.Iio a`). In other words, the theorem asserts that applying the `WithTop.some` function to a set of values in `α` and then taking the set of preimages under `WithTop.some` of the result gives the original set of values. In mathematical terms, it can be written as: $\forall \alpha \in \text{Type } u_1, a \in \alpha: \text{WithTop.some}^{-1}((-\infty, a)) = (-\infty, a)$.
More concisely: For any type `α` and preorder, the preimage under `WithTop.some` of the set of elements in `WithTop α` less than a given element `a` in `α` is equal to the set of elements in `α` less than `a`. In symbols: $\forall \alpha \in \text{Type}, a \in \alpha: \text{WithTop.some}^{-1}((-\infty, a)) = (-\infty, a)$.
|
WithBot.preimage_coe_Ici
theorem WithBot.preimage_coe_Ici :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ici ↑a = Set.Ici a
This theorem states that for any type `α` with a preorder structure and any element `a` of that type, the preimage of the half-closed interval starting at `a` under the canonical map from `α` into `WithBot α` is again the half-closed interval starting at `a`. In mathematical terms, if we consider `WithBot.some` as a function `f: α → WithBot α`, this theorem says that for any `a` in `α`, the set of elements in `α` that `f` maps into the set `{x | a ≤ x}` is exactly the set `{x | a ≤ x}`.
More concisely: For any preordered type `α` and its element `a`, the preimage of the half-closed interval `{x | a ≤ x}` under the canonical map from `α` to `WithBot α` is equal to `{x | a ≤ x}`.
|
WithTop.preimage_coe_Iic
theorem WithTop.preimage_coe_Iic :
∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Iic ↑a = Set.Iic a
The theorem `WithTop.preimage_coe_Iic` asserts that for any given type `α` equipped with a `Preorder` structure, and for any element `a` of type `α`, the preimage of the set of elements less than or equal to `a` (denoted by `Set.Iic ↑a` where `↑a` refers to the lift of `a` to `WithTop α`) under the canonical map `WithTop.some` from `α` to `WithTop α` is exactly the set of elements in `α` that are less than or equal to `a`(denoted `Set.Iic a`). In other words, the canonical map `WithTop.some` perfectly preserves the order structure when considering sets of elements less than or equal to a certain value.
More concisely: For any type `α` with a `Preorder` structure and any element `a` in `α`, the lift of `a` under the canonical map from `α` to `WithTop α` preserves the order relationship, i.e., `Set.Iic (WithTop.some a) = Set.Iic a`.
|