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