Documentation

Mathlib.Data.Set.Intervals.WithBotTop

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} :
WithTop.some ⁻¹' {} =
theorem WithTop.range_coe {α : Type u_1} [PartialOrder α] :
Set.range WithTop.some = Set.Iio
@[simp]
theorem WithTop.preimage_coe_Ioi {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Ioi a = Set.Ioi a
@[simp]
theorem WithTop.preimage_coe_Ici {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Ici a = Set.Ici a
@[simp]
theorem WithTop.preimage_coe_Iio {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Iio a = Set.Iio a
@[simp]
theorem WithTop.preimage_coe_Iic {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Iic a = Set.Iic a
@[simp]
theorem WithTop.preimage_coe_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some ⁻¹' Set.Icc a b = Set.Icc a b
@[simp]
theorem WithTop.preimage_coe_Ico {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some ⁻¹' Set.Ico a b = Set.Ico a b
@[simp]
theorem WithTop.preimage_coe_Ioc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some ⁻¹' Set.Ioc a b = Set.Ioc a b
@[simp]
theorem WithTop.preimage_coe_Ioo {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some ⁻¹' Set.Ioo a b = Set.Ioo a b
@[simp]
theorem WithTop.preimage_coe_Iio_top {α : Type u_1} [PartialOrder α] :
WithTop.some ⁻¹' Set.Iio = Set.univ
@[simp]
theorem WithTop.preimage_coe_Ico_top {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Ico a = Set.Ici a
@[simp]
theorem WithTop.preimage_coe_Ioo_top {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some ⁻¹' Set.Ioo a = Set.Ioi a
theorem WithTop.image_coe_Ioi {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some '' Set.Ioi a = Set.Ioo a
theorem WithTop.image_coe_Ici {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some '' Set.Ici a = Set.Ico a
theorem WithTop.image_coe_Iio {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some '' Set.Iio a = Set.Iio a
theorem WithTop.image_coe_Iic {α : Type u_1} [PartialOrder α] {a : α} :
WithTop.some '' Set.Iic a = Set.Iic a
theorem WithTop.image_coe_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some '' Set.Icc a b = Set.Icc a b
theorem WithTop.image_coe_Ico {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some '' Set.Ico a b = Set.Ico a b
theorem WithTop.image_coe_Ioc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some '' Set.Ioc a b = Set.Ioc a b
theorem WithTop.image_coe_Ioo {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithTop.some '' Set.Ioo a b = Set.Ioo a b

WithBot #

@[simp]
theorem WithBot.preimage_coe_bot {α : Type u_1} :
WithBot.some ⁻¹' {} =
theorem WithBot.range_coe {α : Type u_1} [PartialOrder α] :
Set.range WithBot.some = Set.Ioi
@[simp]
theorem WithBot.preimage_coe_Ioi {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Ioi a = Set.Ioi a
@[simp]
theorem WithBot.preimage_coe_Ici {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Ici a = Set.Ici a
@[simp]
theorem WithBot.preimage_coe_Iio {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Iio a = Set.Iio a
@[simp]
theorem WithBot.preimage_coe_Iic {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Iic a = Set.Iic a
@[simp]
theorem WithBot.preimage_coe_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some ⁻¹' Set.Icc a b = Set.Icc a b
@[simp]
theorem WithBot.preimage_coe_Ico {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some ⁻¹' Set.Ico a b = Set.Ico a b
@[simp]
theorem WithBot.preimage_coe_Ioc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some ⁻¹' Set.Ioc a b = Set.Ioc a b
@[simp]
theorem WithBot.preimage_coe_Ioo {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some ⁻¹' Set.Ioo a b = Set.Ioo a b
@[simp]
theorem WithBot.preimage_coe_Ioi_bot {α : Type u_1} [PartialOrder α] :
WithBot.some ⁻¹' Set.Ioi = Set.univ
@[simp]
theorem WithBot.preimage_coe_Ioc_bot {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Ioc a = Set.Iic a
@[simp]
theorem WithBot.preimage_coe_Ioo_bot {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some ⁻¹' Set.Ioo a = Set.Iio a
theorem WithBot.image_coe_Iio {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some '' Set.Iio a = Set.Ioo a
theorem WithBot.image_coe_Iic {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some '' Set.Iic a = Set.Ioc a
theorem WithBot.image_coe_Ioi {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some '' Set.Ioi a = Set.Ioi a
theorem WithBot.image_coe_Ici {α : Type u_1} [PartialOrder α] {a : α} :
WithBot.some '' Set.Ici a = Set.Ici a
theorem WithBot.image_coe_Icc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some '' Set.Icc a b = Set.Icc a b
theorem WithBot.image_coe_Ioc {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some '' Set.Ioc a b = Set.Ioc a b
theorem WithBot.image_coe_Ico {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some '' Set.Ico a b = Set.Ico a b
theorem WithBot.image_coe_Ioo {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
WithBot.some '' Set.Ioo a b = Set.Ioo a b