# Documentation

Mathlib.Order.Bounds.OrderIso

# Order isomorphisms and bounds. #

theorem OrderIso.upperBounds_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} :
upperBounds (().toEmbedding '' s) = ().toEmbedding ''
theorem OrderIso.lowerBounds_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} :
lowerBounds (().toEmbedding '' s) = ().toEmbedding ''
@[simp]
theorem OrderIso.isLUB_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} {x : β} :
IsLUB (().toEmbedding '' s) x IsLUB s (().toEmbedding x)
theorem OrderIso.isLUB_image' {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} {x : α} :
IsLUB (().toEmbedding '' s) (().toEmbedding x) IsLUB s x
@[simp]
theorem OrderIso.isGLB_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} {x : β} :
IsGLB (().toEmbedding '' s) x IsGLB s (().toEmbedding x)
theorem OrderIso.isGLB_image' {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α ≃o β) {s : Set α} {x : α} :
IsGLB (().toEmbedding '' s) (().toEmbedding x) IsGLB s x
@[simp]
theorem OrderIso.isLUB_preimage {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α ≃o β) {s : Set β} {x : α} :
IsLUB (().toEmbedding ⁻¹' s) x IsLUB s (().toEmbedding x)
theorem OrderIso.isLUB_preimage' {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α ≃o β) {s : Set β} {x : β} :
IsLUB (().toEmbedding ⁻¹' s) (().toEmbedding x) IsLUB s x
@[simp]
theorem OrderIso.isGLB_preimage {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α ≃o β) {s : Set β} {x : α} :
IsGLB (().toEmbedding ⁻¹' s) x IsGLB s (().toEmbedding x)
theorem OrderIso.isGLB_preimage' {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] (f : α ≃o β) {s : Set β} {x : β} :
IsGLB (().toEmbedding ⁻¹' s) (().toEmbedding x) IsGLB s x