Preimages of intervals under order embeddings

In this file we prove that the preimage of an interval in the codomain under an OrderEmbedding is an interval in the domain.

Note that similar statements about images require the range to be order-connected.

@[simp]

theorem OrderEmbedding.preimage_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) : ⇑e ⁻¹' Set.Ici (e x) = Set.Ici x

@[simp]

theorem OrderEmbedding.preimage_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) : ⇑e ⁻¹' Set.Iic (e x) = Set.Iic x

@[simp]

theorem OrderEmbedding.preimage_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) : ⇑e ⁻¹' Set.Ioi (e x) = Set.Ioi x

@[simp]

theorem OrderEmbedding.preimage_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) : ⇑e ⁻¹' Set.Iio (e x) = Set.Iio x

@[simp]

theorem OrderEmbedding.preimage_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Set.Icc (e x) (e y) = Set.Icc x y

@[simp]

theorem OrderEmbedding.preimage_Ico {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Set.Ico (e x) (e y) = Set.Ico x y

@[simp]

theorem OrderEmbedding.preimage_Ioc {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Set.Ioc (e x) (e y) = Set.Ioc x y

@[simp]

theorem OrderEmbedding.preimage_Ioo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Set.Ioo (e x) (e y) = Set.Ioo x y

@[simp]

theorem OrderEmbedding.preimage_uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Set.uIcc (e x) (e y) = Set.uIcc x y

@[simp]

theorem OrderEmbedding.preimage_uIoc {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (e : α ↪o β) (x : α) (y : α) : ⇑e ⁻¹' Ι (e x) (e y) = Ι x y