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