mathlib3 documentation

data.set.intervals.with_bot_top

Intervals in with_top α and with_bot α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove various lemmas about set.images and set.preimages of intervals under coe : α → with_top α and coe : α → with_bot α.

with_top #

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

with_bot #

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