Intervals in WithTop α and WithBot α

In this file we prove various lemmas about Set.images and Set.preimages of intervals under some : α → WithTop α and some : α → WithBot α.

WithTop

@[simp]

theorem WithTop.preimage_coe_top {α : Type u_1} : some ⁻¹' {⊤} = ∅

theorem WithTop.range_coe {α : Type u_1} [Preorder α] : Set.range some = Set.Iio ⊤

@[simp]

theorem WithTop.preimage_coe_Ioi {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ioi ↑a = Set.Ioi a

@[simp]

theorem WithTop.preimage_coe_Ici {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ici ↑a = Set.Ici a

@[simp]

theorem WithTop.preimage_coe_Iio {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Iio ↑a = Set.Iio a

@[simp]

theorem WithTop.preimage_coe_Iic {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Iic ↑a = Set.Iic a

@[simp]

theorem WithTop.preimage_coe_Icc {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b

@[simp]

theorem WithTop.preimage_coe_Ico {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b

@[simp]

theorem WithTop.preimage_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b

@[simp]

theorem WithTop.preimage_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b

@[simp]

theorem WithTop.preimage_coe_Iio_top {α : Type u_1} [Preorder α] : some ⁻¹' Set.Iio ⊤ = Set.univ

@[simp]

theorem WithTop.preimage_coe_Ico_top {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ico ↑a ⊤ = Set.Ici a

@[simp]

theorem WithTop.preimage_coe_Ioo_top {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ioo ↑a ⊤ = Set.Ioi a

theorem WithTop.image_coe_Ioi {α : Type u_1} [Preorder α] {a : α} : some '' Set.Ioi a = Set.Ioo ↑a ⊤

theorem WithTop.image_coe_Ici {α : Type u_1} [Preorder α] {a : α} : some '' Set.Ici a = Set.Ico ↑a ⊤

theorem WithTop.image_coe_Iio {α : Type u_1} [Preorder α] {a : α} : some '' Set.Iio a = Set.Iio ↑a

theorem WithTop.image_coe_Iic {α : Type u_1} [Preorder α] {a : α} : some '' Set.Iic a = Set.Iic ↑a

theorem WithTop.image_coe_Icc {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Icc a b = Set.Icc ↑a ↑b

theorem WithTop.image_coe_Ico {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ico a b = Set.Ico ↑a ↑b

theorem WithTop.image_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ioc a b = Set.Ioc ↑a ↑b

theorem WithTop.image_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ioo a b = Set.Ioo ↑a ↑b

theorem WithTop.Ioi_coe {α : Type u_1} [Preorder α] {a : α} : Set.Ioi ↑a = some '' Set.Ioi a ∪ {⊤}

theorem WithTop.Ici_coe {α : Type u_1} [Preorder α] {a : α} : Set.Ici ↑a = some '' Set.Ici a ∪ {⊤}

theorem WithTop.Iio_coe {α : Type u_1} [Preorder α] {a : α} : Set.Iio ↑a = some '' Set.Iio a

theorem WithTop.Iic_coe {α : Type u_1} [Preorder α] {a : α} : Set.Iic ↑a = some '' Set.Iic a

theorem WithTop.Icc_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Icc ↑a ↑b = some '' Set.Icc a b

theorem WithTop.Ico_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ico ↑a ↑b = some '' Set.Ico a b

theorem WithTop.Ioc_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc ↑a ↑b = some '' Set.Ioc a b

theorem WithTop.Ioo_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo ↑a ↑b = some '' Set.Ioo a b

WithBot

@[simp]

theorem WithBot.preimage_coe_bot {α : Type u_1} : some ⁻¹' {⊥} = ∅

theorem WithBot.range_coe {α : Type u_1} [Preorder α] : Set.range some = Set.Ioi ⊥

@[simp]

theorem WithBot.preimage_coe_Ioi {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ioi ↑a = Set.Ioi a

@[simp]

theorem WithBot.preimage_coe_Ici {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ici ↑a = Set.Ici a

@[simp]

theorem WithBot.preimage_coe_Iio {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Iio ↑a = Set.Iio a

@[simp]

theorem WithBot.preimage_coe_Iic {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Iic ↑a = Set.Iic a

@[simp]

theorem WithBot.preimage_coe_Icc {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b

@[simp]

theorem WithBot.preimage_coe_Ico {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b

@[simp]

theorem WithBot.preimage_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b

@[simp]

theorem WithBot.preimage_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} : some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b

@[simp]

theorem WithBot.preimage_coe_Ioi_bot {α : Type u_1} [Preorder α] : some ⁻¹' Set.Ioi ⊥ = Set.univ

@[simp]

theorem WithBot.preimage_coe_Ioc_bot {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ioc ⊥ ↑a = Set.Iic a

@[simp]

theorem WithBot.preimage_coe_Ioo_bot {α : Type u_1} [Preorder α] {a : α} : some ⁻¹' Set.Ioo ⊥ ↑a = Set.Iio a

theorem WithBot.image_coe_Iio {α : Type u_1} [Preorder α] {a : α} : some '' Set.Iio a = Set.Ioo ⊥ ↑a

theorem WithBot.image_coe_Iic {α : Type u_1} [Preorder α] {a : α} : some '' Set.Iic a = Set.Ioc ⊥ ↑a

theorem WithBot.image_coe_Ioi {α : Type u_1} [Preorder α] {a : α} : some '' Set.Ioi a = Set.Ioi ↑a

theorem WithBot.image_coe_Ici {α : Type u_1} [Preorder α] {a : α} : some '' Set.Ici a = Set.Ici ↑a

theorem WithBot.image_coe_Icc {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Icc a b = Set.Icc ↑a ↑b

theorem WithBot.image_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ioc a b = Set.Ioc ↑a ↑b

theorem WithBot.image_coe_Ico {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ico a b = Set.Ico ↑a ↑b

theorem WithBot.image_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} : some '' Set.Ioo a b = Set.Ioo ↑a ↑b

theorem WithBot.Ioi_coe {α : Type u_1} [Preorder α] {a : α} : Set.Ioi ↑a = some '' Set.Ioi a

theorem WithBot.Ici_coe {α : Type u_1} [Preorder α] {a : α} : Set.Ici ↑a = some '' Set.Ici a

theorem WithBot.Iio_coe {α : Type u_1} [Preorder α] {a : α} : Set.Iio ↑a = some '' Set.Iio a ∪ {⊥}

theorem WithBot.Iic_coe {α : Type u_1} [Preorder α] {a : α} : Set.Iic ↑a = some '' Set.Iic a ∪ {⊥}

theorem WithBot.Icc_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Icc ↑a ↑b = some '' Set.Icc a b

theorem WithBot.Ico_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ico ↑a ↑b = some '' Set.Ico a b

theorem WithBot.Ioc_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ioc ↑a ↑b = some '' Set.Ioc a b

theorem WithBot.Ioo_coe {α : Type u_1} [Preorder α] {a b : α} : Set.Ioo ↑a ↑b = some '' Set.Ioo a b