mathlib3 documentation

data.set.intervals.order_iso

Lemmas about images of intervals under order isomorphisms. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp]
theorem order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.image_Iic {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
⇑e '' set.Iic a = set.Iic (⇑e a)
source
@[simp]
theorem order_iso.image_Ici {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
⇑e '' set.Ici a = set.Ici (⇑e a)
source
@[simp]
theorem order_iso.image_Iio {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
⇑e '' set.Iio a = set.Iio (⇑e a)
source
@[simp]
theorem order_iso.image_Ioi {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (e : α ≃o β) (a : α) :
⇑e '' set.Ioi a = set.Ioi (⇑e a)
source
@[simp]
theorem order_iso.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 order_iso.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 order_iso.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 order_iso.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 order_iso.Iic_top {α : Type u_1} [preorder α] [order_top α] :
↥(set.Iic ⊤) ≃o α

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

Equations
source
def order_iso.Ici_bot {α : Type u_1} [preorder α] [order_bot α] :
↥(set.Ici ⊥) ≃o α

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

Equations