OrderEmbedding.preimage_Ioc
theorem OrderEmbedding.preimage_Ioc :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
⇑e ⁻¹' Set.Ioc (e x) (e y) = Set.Ioc x y
The theorem `OrderEmbedding.preimage_Ioc` states that for any two types `α` and `β` with a preorder relation, and for any order-embedding `e` from `α` to `β`, the preimage of the left-open right-closed interval `(e x, e y]` under the embedding `e` equals the interval `(x, y]` in `α`. In other words, if you apply `e` to each element in the interval `(x, y]` and then take the preimage under `e`, you get the interval `(x, y]` back.
More concisely: For any order-embedding `e` between types `α` and `β` with preorder relations, the preimage of the interval `(e x, e y]` in `β` is equal to the interval `(x, y]` in `α`.
|
OrderEmbedding.preimage_Icc
theorem OrderEmbedding.preimage_Icc :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) (x y : α),
⇑e ⁻¹' Set.Icc (e x) (e y) = Set.Icc x y
The theorem `OrderEmbedding.preimage_Icc` states that for all types `α` and `β` which have a preorder relationship (meaning that they can be compared in a certain way), and for all order embeddings `e` from `α` into `β`, and any two elements `x` and `y` of `α`, the preimage of the closed interval `[e(x), e(y)]` under the map `e` is precisely the closed interval `[x, y]` in `α`.
In other words, if we apply the order-embedding `e` to the elements of the interval `[x, y]` in `α`, and then take the preimage under `e`, we will recover the original interval `[x, y]`. This theorem shows the preservation of the closed interval under the order-embedding and its inverse.
More concisely: For any preorder types `α` and `β`, and order embedding `e` from `α` to `β`, the preimage of an interval `[e(x), e(y)]` in `β` under `e` is equal to the interval `[x, y]` in `α`.
|