# Documentation

Mathlib.Data.Set.Intervals.OrderIso

# Lemmas about images of intervals under order isomorphisms. #

@[simp]
theorem OrderIso.preimage_Iic {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (b : β) :
().toEmbedding ⁻¹' = Set.Iic (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (b : β) :
().toEmbedding ⁻¹' = Set.Ici (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Iio {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (b : β) :
().toEmbedding ⁻¹' = Set.Iio (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Ioi {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (b : β) :
().toEmbedding ⁻¹' = Set.Ioi (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Icc {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : β) (b : β) :
().toEmbedding ⁻¹' Set.Icc a b = Set.Icc (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Ico {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : β) (b : β) :
().toEmbedding ⁻¹' Set.Ico a b = Set.Ico (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Ioc {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : β) (b : β) :
().toEmbedding ⁻¹' Set.Ioc a b = Set.Ioc (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.preimage_Ioo {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : β) (b : β) :
().toEmbedding ⁻¹' Set.Ioo a b = Set.Ioo (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.image_Iic {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) :
().toEmbedding '' = Set.Iic (().toEmbedding a)
@[simp]
theorem OrderIso.image_Ici {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) :
().toEmbedding '' = Set.Ici (().toEmbedding a)
@[simp]
theorem OrderIso.image_Iio {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) :
().toEmbedding '' = Set.Iio (().toEmbedding a)
@[simp]
theorem OrderIso.image_Ioi {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) :
().toEmbedding '' = Set.Ioi (().toEmbedding a)
@[simp]
theorem OrderIso.image_Ioo {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) (b : α) :
().toEmbedding '' Set.Ioo a b = Set.Ioo (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.image_Ioc {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) (b : α) :
().toEmbedding '' Set.Ioc a b = Set.Ioc (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.image_Ico {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) (b : α) :
().toEmbedding '' Set.Ico a b = Set.Ico (().toEmbedding a) (().toEmbedding b)
@[simp]
theorem OrderIso.image_Icc {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (e : α ≃o β) (a : α) (b : α) :
().toEmbedding '' Set.Icc a b = Set.Icc (().toEmbedding a) (().toEmbedding b)
def OrderIso.IicTop {α : Type u_1} [inst : ] [inst : ] :
↑() ≃o α

Order isomorphism between Iic (⊤ : α)⊤ : α) and α when α has a top element

Equations
• One or more equations did not get rendered due to their size.
def OrderIso.IciBot {α : Type u_1} [inst : ] [inst : ] :
↑() ≃o α

Order isomorphism between Ici (⊥ : α)⊥ : α) and α when α has a bottom element

Equations
• One or more equations did not get rendered due to their size.