HepLean Documentation

Mathlib.Order.Interval.Set.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 #

source
@[simp]
theorem WithTop.preimage_coe_top {α : Type u_1} :
WithTop.some ⁻¹' {⊤} = ∅
source
theorem WithTop.range_coe {α : Type u_1} [Preorder α] :
Set.range WithTop.some = Set.Iio ⊤
source
@[simp]
theorem WithTop.preimage_coe_Ioi {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
source
@[simp]
theorem WithTop.preimage_coe_Ici {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Ici ↑a = Set.Ici a
source
@[simp]
theorem WithTop.preimage_coe_Iio {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Iio ↑a = Set.Iio a
source
@[simp]
theorem WithTop.preimage_coe_Iic {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Iic ↑a = Set.Iic a
source
@[simp]
theorem WithTop.preimage_coe_Icc {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
source
@[simp]
theorem WithTop.preimage_coe_Ico {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
source
@[simp]
theorem WithTop.preimage_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
source
@[simp]
theorem WithTop.preimage_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
source
@[simp]
theorem WithTop.preimage_coe_Iio_top {α : Type u_1} [Preorder α] :
WithTop.some ⁻¹' Set.Iio ⊤ = Set.univ
source
@[simp]
theorem WithTop.preimage_coe_Ico_top {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Ico ↑a ⊤ = Set.Ici a
source
@[simp]
theorem WithTop.preimage_coe_Ioo_top {α : Type u_1} [Preorder α] {a : α} :
WithTop.some ⁻¹' Set.Ioo ↑a ⊤ = Set.Ioi a
source
theorem WithTop.image_coe_Ioi {α : Type u_1} [Preorder α] {a : α} :
WithTop.some '' Set.Ioi a = Set.Ioo ↑a ⊤
source
theorem WithTop.image_coe_Ici {α : Type u_1} [Preorder α] {a : α} :
WithTop.some '' Set.Ici a = Set.Ico ↑a ⊤
source
theorem WithTop.image_coe_Iio {α : Type u_1} [Preorder α] {a : α} :
WithTop.some '' Set.Iio a = Set.Iio ↑a
source
theorem WithTop.image_coe_Iic {α : Type u_1} [Preorder α] {a : α} :
WithTop.some '' Set.Iic a = Set.Iic ↑a
source
theorem WithTop.image_coe_Icc {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some '' Set.Icc a b = Set.Icc ↑a ↑b
source
theorem WithTop.image_coe_Ico {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some '' Set.Ico a b = Set.Ico ↑a ↑b
source
theorem WithTop.image_coe_Ioc {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some '' Set.Ioc a b = Set.Ioc ↑a ↑b
source
theorem WithTop.image_coe_Ioo {α : Type u_1} [Preorder α] {a b : α} :
WithTop.some '' Set.Ioo a b = Set.Ioo ↑a ↑b

WithBot #

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