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