Documentation

Mathlib.Order.Bounds.OrderIso

Order isomorphisms and bounds. #

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