# Lemmas about images of intervals under order isomorphisms. #

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

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

Equations

- OrderIso.IicTop = { toEquiv := Equiv.subtypeUnivEquiv ⋯, map_rel_iff' := ⋯ }

Instances For

source
def OrderIso.IciBot {α : Type u_1} [Preorder α] [OrderBot α] :
↑(Set.Ici ⊥) ≃o α

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

Equations

- OrderIso.IciBot = { toEquiv := Equiv.subtypeUnivEquiv ⋯, map_rel_iff' := ⋯ }

Instances For