OrderIso.isLUB_image
theorem OrderIso.isLUB_image :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α} {x : β},
IsLUB (⇑f '' s) x ↔ IsLUB s (f.symm x)
This theorem states that for any given preorder types `α` and `β`, and a order isomorphism `f` from `α` to `β`, a particular element `x` from `β` is a least upper bound of the image set of `s` under `f` if and only if the inverse image of `x` under `f` (denoted as `(OrderIso.symm f) x`) is a least upper bound of the original set `s` in `α`. In other words, the least upper bound property is preserved under the order isomorphism and its inverse.
More concisely: For any preorders types `α` and `β`, and an order isomorphism `f` from `α` to `β`, the element `x` in `β` is the least upper bound of `f(s)` if and only if `(OrderIso.symm f) x` is the least upper bound of `s` in `α`.
|
OrderIso.upperBounds_image
theorem OrderIso.upperBounds_image :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set α},
upperBounds (⇑f '' s) = ⇑f '' upperBounds s
This theorem states that for any two types `α` and `β` equipped with a preorder structure, and given an order isomorphism `f` from `α` to `β`, the image under `f` of the set of upper bounds of a set `s` in `α` is equal to the set of upper bounds of the image of `s` under `f` in `β`. In simpler terms, this theorem asserts that the order isomorphism `f` preserves the property of being an upper bound of a set when applied to both the elements of the set and its upper bounds.
More concisely: Given types `α` and `β` with preorders, an order isomorphism `f` from `α` to `β`, and a set `s` in `α`, the image of the set of upper bounds of `s` under `f` equals the set of upper bounds of `f(s)` in `β`.
|
OrderIso.isLUB_preimage
theorem OrderIso.isLUB_preimage :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : α},
IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)
The theorem `OrderIso.isLUB_preimage` states that for any types `α` and `β` with preorder structures, any order isomorphism `f` from `α` to `β`, any set `s` of type `β`, and any element `x` of type `α`, `x` is a least upper bound of the preimage of `s` under `f` if and only if `f(x)` is a least upper bound of `s`. This theorem essentially asserts the preservation of least upper bounds under order isomorphisms.
More concisely: For any preorders on types `α` and `β`, order isomorphism `f` from `α` to `β`, set `s` in `β`, and element `x` in `α`, if `x` is the least upper bound of `f''{s} (the preimage of `s` under `f`) then `f(x)` is the least upper bound of `s`.
|
OrderIso.isLUB_preimage'
theorem OrderIso.isLUB_preimage' :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : β},
IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x
This theorem states that for any order isomorphism `f` between two partially ordered sets `α` and `β`, and for any set `s` of elements in `β` and any element `x` in `β`, `x` is a least upper bound of set `s` if and only if the inverse image of `x` under `f`, denoted as `OrderIso.symm f x`, is a least upper bound of the inverse image of `s` under `f`, denoted as `f ⁻¹' s`. Essentially, it says that the property of being a least upper bound is preserved under the inverse of an order isomorphism.
More concisely: For any order isomorphism between two partially ordered sets, the inverse image of a least upper bound is a least upper bound for the inverse image under that isomorphism.
|