OrderIso.image_eq_preimage
theorem OrderIso.image_eq_preimage :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set α), ⇑e '' s = ⇑e.symm ⁻¹' s
This theorem states that for any ordered types `α` and `β`, given an order isomorphism `e` from `α` to `β` and a set `s` in `α`, the image of `s` under `e` is equal to the preimage of `s` under the inverse of `e`. In other words, applying the order isomorphism `e` to each element of set `s` provides the same set as if you were to apply the inverse of `e` to each element of set `s` and consider their pre-images in `α`.
More concisely: For any order isomorphism between ordered types `α` and `β`, and any set `s` in `α`, the forward and inverse images of `s` under this isomorphism are equal: `e(s) = {x | ∃y ∈ s, e(y) = x}`.
|
OrderIso.image_preimage
theorem OrderIso.image_preimage :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set β), ⇑e '' (⇑e ⁻¹' s) = s := by
sorry
The theorem `OrderIso.image_preimage` states that for any two ordered types `α` and `β`, given an order isomorphism `e` from `α` to `β` and a set `s` of type `β`, the image under `e` of the preimage under `e` of `s` is equal to `s` itself. In other words, if we first map elements of `β` back to `α` through the isomorphism `e` and then map them forward to `β` again, we end up with the original set `s`.
More concisely: For any order isomorphism `e` between ordered types `α` and `β` and any set `s` of type `β`, `e''(e��мпи(s)) = s`.
|