mathlib documentation

data.set.intervals.with_bot_top

Intervals in with_top α and with_bot α #

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} :
theorem with_top.range_coe {α : Type u_1} [partial_order α] :
@[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]
theorem with_top.preimage_coe_Ico_top {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_top.preimage_coe_Ioo_top {α : Type u_1} [partial_order α] {a : α} :
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} :
theorem with_bot.range_coe {α : Type u_1} [partial_order α] :
@[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]
theorem with_bot.preimage_coe_Ioc_bot {α : Type u_1} [partial_order α] {a : α} :
@[simp]
theorem with_bot.preimage_coe_Ioo_bot {α : Type u_1} [partial_order α] {a : α} :
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 : α} :