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 #

@[simp]
theorem with_top.preimage_coe_top {α : Type u_1} :
@[simp]
theorem with_top.preimage_coe_Ioi {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_top.preimage_coe_Ici {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_top.preimage_coe_Iio {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_top.preimage_coe_Iic {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_top.preimage_coe_Icc {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_top.preimage_coe_Ico {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_top.preimage_coe_Ioc {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_top.preimage_coe_Ioo {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
@[simp]
theorem with_top.image_coe_Ioi {α : Type u_1} [partial_order α] {a : α} :
theorem with_top.image_coe_Ici {α : Type u_1} [partial_order α] {a : α} :
theorem with_top.image_coe_Iio {α : Type u_1} [partial_order α] {a : α} :
theorem with_top.image_coe_Iic {α : Type u_1} [partial_order α] {a : α} :
theorem with_top.image_coe_Icc {α : Type u_1} [partial_order α] {a b : α} :
theorem with_top.image_coe_Ico {α : Type u_1} [partial_order α] {a b : α} :
theorem with_top.image_coe_Ioc {α : Type u_1} [partial_order α] {a b : α} :
theorem with_top.image_coe_Ioo {α : Type u_1} [partial_order α] {a b : α} :

with_bot #

@[simp]
theorem with_bot.preimage_coe_bot {α : Type u_1} :
@[simp]
theorem with_bot.preimage_coe_Ioi {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_bot.preimage_coe_Ici {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_bot.preimage_coe_Iio {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_bot.preimage_coe_Iic {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_bot.preimage_coe_Icc {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_bot.preimage_coe_Ico {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_bot.preimage_coe_Ioc {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
theorem with_bot.preimage_coe_Ioo {α : Type u_1} [partial_order α] {a b : α} :
@[simp]
@[simp]
theorem with_bot.image_coe_Iio {α : Type u_1} [partial_order α] {a : α} :
theorem with_bot.image_coe_Iic {α : Type u_1} [partial_order α] {a : α} :
theorem with_bot.image_coe_Ioi {α : Type u_1} [partial_order α] {a : α} :
theorem with_bot.image_coe_Ici {α : Type u_1} [partial_order α] {a : α} :
theorem with_bot.image_coe_Icc {α : Type u_1} [partial_order α] {a b : α} :
theorem with_bot.image_coe_Ioc {α : Type u_1} [partial_order α] {a b : α} :
theorem with_bot.image_coe_Ico {α : Type u_1} [partial_order α] {a b : α} :
theorem with_bot.image_coe_Ioo {α : Type u_1} [partial_order α] {a b : α} :