WithBotTop

📁 Source: Mathlib/Order/Interval/Set/WithBotTop.lean

Statistics

Metric	Count
Definitions	0
Theorems `Icc_coe`, `Ici_coe`, `Ico_coe`, `Iic_coe`, `Iio_coe`, `Ioc_coe`, `Ioi_coe`, `Ioo_coe`, `image_coe_Icc`, `image_coe_Ici`, `image_coe_Ico`, `image_coe_Iic`, `image_coe_Iio`, `image_coe_Ioc`, `image_coe_Ioi`, `image_coe_Ioo`, `preimage_coe_Icc`, `preimage_coe_Ici`, `preimage_coe_Ico`, `preimage_coe_Iic`, `preimage_coe_Iio`, `preimage_coe_Ioc`, `preimage_coe_Ioc_bot`, `preimage_coe_Ioi`, `preimage_coe_Ioi_bot`, `preimage_coe_Ioo`, `preimage_coe_Ioo_bot`, `preimage_coe_bot`, `range_coe`, `Icc_coe`, `Ici_coe`, `Ico_coe`, `Iic_coe`, `Iio_coe`, `Ioc_coe`, `Ioi_coe`, `Ioo_coe`, `image_coe_Icc`, `image_coe_Ici`, `image_coe_Ico`, `image_coe_Iic`, `image_coe_Iio`, `image_coe_Ioc`, `image_coe_Ioi`, `image_coe_Ioo`, `preimage_coe_Icc`, `preimage_coe_Ici`, `preimage_coe_Ico`, `preimage_coe_Ico_top`, `preimage_coe_Iic`, `preimage_coe_Iio`, `preimage_coe_Iio_top`, `preimage_coe_Ioc`, `preimage_coe_Ioi`, `preimage_coe_Ioo`, `preimage_coe_Ioo_top`, `preimage_coe_top`, `range_coe`	58
Total	58

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_coe` 📖	mathematical	—	`Set.Icc` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Icc`
`Ici_coe` 📖	mathematical	—	`Set.Ici` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Ici`
`Ico_coe` 📖	mathematical	—	`Set.Ico` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Ico`
`Iic_coe` 📖	mathematical	—	`Set.Iic` `WithBot` `instPreorder` `some` `Set` `Set.instUnion` `Set.image` `Set.instSingletonSet` `Bot.bot` `bot`	—	`Set.ext` `Set.union_singleton`
`Iio_coe` 📖	mathematical	—	`Set.Iio` `WithBot` `instPreorder` `some` `Set` `Set.instUnion` `Set.image` `Set.instSingletonSet` `Bot.bot` `bot`	—	`Set.ext` `Set.union_singleton`
`Ioc_coe` 📖	mathematical	—	`Set.Ioc` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Ioc`
`Ioi_coe` 📖	mathematical	—	`Set.Ioi` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Ioi`
`Ioo_coe` 📖	mathematical	—	`Set.Ioo` `WithBot` `instPreorder` `some` `Set.image`	—	`image_coe_Ioo`
`image_coe_Icc` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Icc` `instPreorder`	—	`preimage_coe_Icc` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Icc_subset_Ici_self` `Set.Ici_subset_Ioi` `bot_lt_coe`
`image_coe_Ici` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Ici` `instPreorder`	—	`preimage_coe_Ici` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Ici_subset_Ioi` `bot_lt_coe`
`image_coe_Ico` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Ico` `instPreorder`	—	`preimage_coe_Ico` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ico_subset_Ici_self` `Set.Ici_subset_Ioi` `bot_lt_coe`
`image_coe_Iic` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Iic` `Set.Ioc` `instPreorder` `Bot.bot` `bot`	—	`preimage_coe_Iic` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_comm` `Set.Ioi_inter_Iic`
`image_coe_Iio` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Iio` `Set.Ioo` `instPreorder` `Bot.bot` `bot`	—	`preimage_coe_Iio` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_comm` `Set.Ioi_inter_Iio`
`image_coe_Ioc` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Ioc` `instPreorder`	—	`preimage_coe_Ioc` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ioc_subset_Ioi_self` `Set.Ioi_subset_Ioi` `bot_le`
`image_coe_Ioi` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Ioi` `instPreorder`	—	`preimage_coe_Ioi` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Ioi_subset_Ioi` `bot_le`
`image_coe_Ioo` 📖	mathematical	—	`Set.image` `WithBot` `some` `Set.Ioo` `instPreorder`	—	`preimage_coe_Ioo` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ioo_subset_Ioi_self` `Set.Ioi_subset_Ioi` `bot_le`
`preimage_coe_Icc` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Icc` `instPreorder`	—	`preimage_coe_Ici` `preimage_coe_Iic`
`preimage_coe_Ici` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ici` `instPreorder`	—	`Set.ext` `coe_le_coe`
`preimage_coe_Ico` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ico` `instPreorder`	—	`preimage_coe_Ici` `preimage_coe_Iio`
`preimage_coe_Iic` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Iic` `instPreorder`	—	`Set.ext` `coe_le_coe`
`preimage_coe_Iio` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Iio` `instPreorder`	—	`Set.ext` `coe_lt_coe`
`preimage_coe_Ioc` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioc` `instPreorder`	—	`preimage_coe_Ioi` `preimage_coe_Iic`
`preimage_coe_Ioc_bot` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioc` `instPreorder` `Bot.bot` `bot` `Set.Iic`	—	`preimage_coe_Ioi_bot` `preimage_coe_Iic` `Set.univ_inter`
`preimage_coe_Ioi` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioi` `instPreorder`	—	`Set.ext` `coe_lt_coe`
`preimage_coe_Ioi_bot` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioi` `instPreorder` `Bot.bot` `bot` `Set.univ`	—	`range_coe` `Set.preimage_range`
`preimage_coe_Ioo` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioo` `instPreorder`	—	`preimage_coe_Ioi` `preimage_coe_Iio`
`preimage_coe_Ioo_bot` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set.Ioo` `instPreorder` `Bot.bot` `bot` `Set.Iio`	—	`preimage_coe_Ioi_bot` `preimage_coe_Iio` `Set.univ_inter`
`preimage_coe_bot` 📖	mathematical	—	`Set.preimage` `WithBot` `some` `Set` `Set.instSingletonSet` `Bot.bot` `bot` `Set.instEmptyCollection`	—	`WithTop.preimage_coe_top`
`range_coe` 📖	mathematical	—	`Set.range` `WithBot` `some` `Set.Ioi` `instPreorder` `Bot.bot` `bot`	—	`Set.ext`

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_coe` 📖	mathematical	—	`Set.Icc` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Icc`
`Ici_coe` 📖	mathematical	—	`Set.Ici` `WithTop` `instPreorder` `some` `Set` `Set.instUnion` `Set.image` `Set.instSingletonSet` `Top.top` `top`	—	`Set.ext` `Set.union_singleton`
`Ico_coe` 📖	mathematical	—	`Set.Ico` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Ico`
`Iic_coe` 📖	mathematical	—	`Set.Iic` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Iic`
`Iio_coe` 📖	mathematical	—	`Set.Iio` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Iio`
`Ioc_coe` 📖	mathematical	—	`Set.Ioc` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Ioc`
`Ioi_coe` 📖	mathematical	—	`Set.Ioi` `WithTop` `instPreorder` `some` `Set` `Set.instUnion` `Set.image` `Set.instSingletonSet` `Top.top` `top`	—	`Set.ext` `Set.union_singleton`
`Ioo_coe` 📖	mathematical	—	`Set.Ioo` `WithTop` `instPreorder` `some` `Set.image`	—	`image_coe_Ioo`
`image_coe_Icc` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Icc` `instPreorder`	—	`preimage_coe_Icc` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Icc_subset_Iic_self` `Set.Iic_subset_Iio` `coe_lt_top`
`image_coe_Ici` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Ici` `Set.Ico` `instPreorder` `Top.top` `top`	—	`preimage_coe_Ici` `Set.image_preimage_eq_inter_range` `range_coe` `Set.Ici_inter_Iio`
`image_coe_Ico` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Ico` `instPreorder`	—	`preimage_coe_Ico` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ico_subset_Iio_self` `Set.Iio_subset_Iio` `le_top`
`image_coe_Iic` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Iic` `instPreorder`	—	`preimage_coe_Iic` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Iic_subset_Iio` `coe_lt_top`
`image_coe_Iio` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Iio` `instPreorder`	—	`preimage_coe_Iio` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Iio_subset_Iio` `le_top`
`image_coe_Ioc` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Ioc` `instPreorder`	—	`preimage_coe_Ioc` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ioc_subset_Iic_self` `Set.Iic_subset_Iio` `coe_lt_top`
`image_coe_Ioi` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Ioi` `Set.Ioo` `instPreorder` `Top.top` `top`	—	`preimage_coe_Ioi` `Set.image_preimage_eq_inter_range` `range_coe` `Set.Ioi_inter_Iio`
`image_coe_Ioo` 📖	mathematical	—	`Set.image` `WithTop` `some` `Set.Ioo` `instPreorder`	—	`preimage_coe_Ioo` `Set.image_preimage_eq_inter_range` `range_coe` `Set.inter_eq_self_of_subset_left` `Set.Subset.trans` `Set.Ioo_subset_Iio_self` `Set.Iio_subset_Iio` `le_top`
`preimage_coe_Icc` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Icc` `instPreorder`	—	`preimage_coe_Ici` `preimage_coe_Iic`
`preimage_coe_Ici` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ici` `instPreorder`	—	`Set.ext` `coe_le_coe`
`preimage_coe_Ico` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ico` `instPreorder`	—	`preimage_coe_Ici` `preimage_coe_Iio`
`preimage_coe_Ico_top` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ico` `instPreorder` `Top.top` `top` `Set.Ici`	—	`preimage_coe_Ici` `preimage_coe_Iio_top` `Set.inter_univ`
`preimage_coe_Iic` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Iic` `instPreorder`	—	`Set.ext` `coe_le_coe`
`preimage_coe_Iio` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Iio` `instPreorder`	—	`Set.ext` `coe_lt_coe`
`preimage_coe_Iio_top` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Iio` `instPreorder` `Top.top` `top` `Set.univ`	—	`range_coe` `Set.preimage_range`
`preimage_coe_Ioc` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ioc` `instPreorder`	—	`preimage_coe_Ioi` `preimage_coe_Iic`
`preimage_coe_Ioi` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ioi` `instPreorder`	—	`Set.ext` `coe_lt_coe`
`preimage_coe_Ioo` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ioo` `instPreorder`	—	`preimage_coe_Ioi` `preimage_coe_Iio`
`preimage_coe_Ioo_top` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set.Ioo` `instPreorder` `Top.top` `top` `Set.Ioi`	—	`preimage_coe_Ioi` `preimage_coe_Iio_top` `Set.inter_univ`
`preimage_coe_top` 📖	mathematical	—	`Set.preimage` `WithTop` `some` `Set` `Set.instSingletonSet` `Top.top` `top` `Set.instEmptyCollection`	—	`Set.eq_empty_of_subset_empty` `coe_ne_top`
`range_coe` 📖	mathematical	—	`Set.range` `WithTop` `some` `Set.Iio` `instPreorder` `Top.top` `top`	—	`Set.ext`

---

← Back to Index