Lemmas about images of intervals under order isomorphisms. #
@[simp]
theorem
OrderIso.preimage_Iic
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Iic b = Set.Iic (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Ici
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Ici b = Set.Ici (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Iio
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Iio b = Set.Iio (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Ioi
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Ioi b = Set.Ioi (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Icc
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Icc a b = Set.Icc (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding a)
(↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Ico
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Ico a b = Set.Ico (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding a)
(↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Ioc
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Ioc a b = Set.Ioc (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding a)
(↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.preimage_Ioo
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : β)
(b : β)
:
↑(RelIso.toRelEmbedding e).toEmbedding ⁻¹' Set.Ioo a b = Set.Ioo (↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding a)
(↑(RelIso.toRelEmbedding (OrderIso.symm e)).toEmbedding b)
@[simp]
theorem
OrderIso.image_Iic
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Iic a = Set.Iic (↑(RelIso.toRelEmbedding e).toEmbedding a)
@[simp]
theorem
OrderIso.image_Ici
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Ici a = Set.Ici (↑(RelIso.toRelEmbedding e).toEmbedding a)
@[simp]
theorem
OrderIso.image_Iio
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Iio a = Set.Iio (↑(RelIso.toRelEmbedding e).toEmbedding a)
@[simp]
theorem
OrderIso.image_Ioi
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Ioi a = Set.Ioi (↑(RelIso.toRelEmbedding e).toEmbedding a)
@[simp]
theorem
OrderIso.image_Ioo
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
(b : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Ioo a b = Set.Ioo (↑(RelIso.toRelEmbedding e).toEmbedding a) (↑(RelIso.toRelEmbedding e).toEmbedding b)
@[simp]
theorem
OrderIso.image_Ioc
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
(b : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Ioc a b = Set.Ioc (↑(RelIso.toRelEmbedding e).toEmbedding a) (↑(RelIso.toRelEmbedding e).toEmbedding b)
@[simp]
theorem
OrderIso.image_Ico
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
(b : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Ico a b = Set.Ico (↑(RelIso.toRelEmbedding e).toEmbedding a) (↑(RelIso.toRelEmbedding e).toEmbedding b)
@[simp]
theorem
OrderIso.image_Icc
{α : Type u_1}
{β : Type u_2}
[inst : Preorder α]
[inst : Preorder β]
(e : α ≃o β)
(a : α)
(b : α)
:
↑(RelIso.toRelEmbedding e).toEmbedding '' Set.Icc a b = Set.Icc (↑(RelIso.toRelEmbedding e).toEmbedding a) (↑(RelIso.toRelEmbedding e).toEmbedding b)