Documentation

Mathlib.Order.Bounds.OrderIso

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 (f.symm 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 (f.symm 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) (f.symm 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) (f.symm x) IsGLB s x