OrderIso.preimage_Ioi
theorem OrderIso.preimage_Ioi :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
⇑e ⁻¹' Set.Ioi b = Set.Ioi (e.symm b)
The theorem `OrderIso.preimage_Ioi` states that for any two types `α` and `β` that have a preorder structure (meaning that they have a binary relation which is reflexive and transitive), if there exists an order isomorphism `e` between them, then the preimage of the set of all elements in `β` greater than a given element `b` under `e` is the set of all elements in `α` greater than the inverse image of `b` under the inverse of `e`. In other words, applying the order isomorphism to a right-open infinite interval in `α` maps it to the corresponding right-open infinite interval in `β`.
More concisely: For any preorder structures on types `α` and `β` with an order isomorphism between them, the inverse image of elements greater than `b` in `β` under the isomorphism's inverse is equal to the set of elements greater than the inverse image of `b` in `α`.
|
OrderIso.preimage_Iic
theorem OrderIso.preimage_Iic :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
⇑e ⁻¹' Set.Iic b = Set.Iic (e.symm b)
The theorem `OrderIso.preimage_Iic` states that for any two types `α` and `β` with a preorder relation, and given an order isomorphism `e` between `α` and `β`, the preimage of the left-infinite right-closed interval ending at `b` under the order isomorphism `e` is equal to the left-infinite right-closed interval ending at the inverse of `e` applied to `b`. In other words, the order isomorphism correctly maps the definitions of such intervals between the two ordered sets.
More concisely: Given an order isomorphism between two preordered types, the preimage of a left-infinite right-closed interval under the order isomorphism is the left-infinite right-closed interval with the same endpoint but under the order isomorphism's inverse.
|
OrderIso.preimage_Ici
theorem OrderIso.preimage_Ici :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
⇑e ⁻¹' Set.Ici b = Set.Ici (e.symm b)
This theorem, `OrderIso.preimage_Ici`, states that for any two types `α` and `β` that are both preordered, and for any order isomorphism `e` from `α` to `β` and any element `b` of type `β`, the preimage of the set of elements in `β` that are greater than or equal to `b` under the isomorphism `e` is equal to the set of elements in `α` that are greater than or equal to the element in `α` that `b` maps to under the inverse of the isomorphism `e`. In other words, the order isomorphism preserves the property of being greater than or equal to a certain value.
More concisely: For any preordered types `α` and `β` and order isomorphism `e` from `α` to `β`, the preimage under `e` of the set `{x : β | x ≥ b}` is equal to `{x : α | e x ≥ b}`.
|
OrderIso.preimage_Iio
theorem OrderIso.preimage_Iio :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
⇑e ⁻¹' Set.Iio b = Set.Iio (e.symm b)
The theorem `OrderIso.preimage_Iio` states that for any two types `α` and `β` both having preorder relations and any order isomorphism `e` from `α` to `β` and any element `b` of `β`, the preimage of the left-infinite right-open interval less than `b` under the order isomorphism `e` is equal to the left-infinite right-open interval less than the image of `b` under the inverse of the order isomorphism `e`. In other words, the order isomorphism preserves the structure of these intervals under the inverse mapping.
More concisely: For any order isomorphism between preordered types `α` and `β`, and any `b` in `β`, the preimage under the isomorphism of the left-infinite right-open interval `(-\infty, b)` in `β` is equal to the left-infinite right-open interval `(-\infty, e⁻¹(b))` in `α`.
|