Order isomorphisms and bounds.

theorem OrderIso.upperBounds_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} : upperBounds (↑f '' s) = ↑f '' upperBounds s

theorem OrderIso.lowerBounds_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} : lowerBounds (↑f '' s) = ↑f '' lowerBounds s

@[simp]

theorem OrderIso.isLUB_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : β} : IsLUB (↑f '' s) x ↔ IsLUB s (↑(OrderIso.symm f) x)

theorem OrderIso.isLUB_image' {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : α} : IsLUB (↑f '' s) (↑f x) ↔ IsLUB s x

@[simp]

theorem OrderIso.isGLB_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : β} : IsGLB (↑f '' s) x ↔ IsGLB s (↑(OrderIso.symm f) x)

theorem OrderIso.isGLB_image' {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set α} {x : α} : IsGLB (↑f '' s) (↑f x) ↔ IsGLB s x

@[simp]

theorem OrderIso.isLUB_preimage {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : α} : IsLUB (↑f ⁻¹' s) x ↔ IsLUB s (↑f x)

theorem OrderIso.isLUB_preimage' {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : β} : IsLUB (↑f ⁻¹' s) (↑(OrderIso.symm f) x) ↔ IsLUB s x

@[simp]

theorem OrderIso.isGLB_preimage {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : α} : IsGLB (↑f ⁻¹' s) x ↔ IsGLB s (↑f x)

theorem OrderIso.isGLB_preimage' {α : Type u_2} {β : Type u_1} [Preorder α] [Preorder β] (f : α ≃o β) {s : Set β} {x : β} : IsGLB (↑f ⁻¹' s) (↑(OrderIso.symm f) x) ↔ IsGLB s x