Interval

📁 Source: Mathlib/Data/Finset/Interval.lean

Statistics

Metric	Count
Definitions `instLocallyFiniteOrder`	1
Theorems `Icc_eq_filter_powerset`, `Icc_eq_image_powerset`, `Ico_eq_filter_ssubsets`, `Ico_eq_image_ssubsets`, `Iic_eq_powerset`, `Iio_eq_ssubsets`, `Ioc_eq_filter_powerset`, `Ioo_eq_filter_ssubsets`, `antitone_iff_forall_cons_le`, `antitone_iff_forall_insert_le`, `card_Icc_finset`, `card_Ico_finset`, `card_Iic_finset`, `card_Iio_finset`, `card_Ioc_finset`, `card_Ioo_finset`, `monotone_iff_forall_le_cons`, `monotone_iff_forall_le_insert`, `strictAnti_iff_forall_cons_lt`, `strictAnti_iff_forall_lt_insert`, `strictMono_iff_forall_lt_cons`, `strictMono_iff_forall_lt_insert`	22
Total	23

Finset

Definitions

Name	Category	Theorems
`instLocallyFiniteOrder` 📖	CompOp	14 math math: `Icc_eq_image_powerset`, `card_Ioo_finset`, `Ioo_eq_filter_ssubsets`, `card_Iio_finset`, `Ico_eq_filter_ssubsets`, `card_Icc_finset`, `Ico_eq_image_ssubsets`, `card_Ico_finset`, `Iic_eq_powerset`, `card_Ioc_finset`, `card_Iic_finset`, `Ioc_eq_filter_powerset`, `Iio_eq_ssubsets`, `Icc_eq_filter_powerset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_eq_filter_powerset` 📖	mathematical	—	`Icc` `Finset` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `filter` `instHasSubset` `instDecidableRelSubset` `powerset`	—	`ext`
`Icc_eq_image_powerset` 📖	mathematical	`Finset` `instHasSubset`	`Icc` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `image` `decidableEq` `instUnion` `powerset` `instSDiff`	—	`ext` `disjUnion_eq_union` `union_comm`
`Ico_eq_filter_ssubsets` 📖	mathematical	—	`Ico` `Finset` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `filter` `instHasSubset` `instDecidableRelSubset` `ssubsets`	—	`ext`
`Ico_eq_image_ssubsets` 📖	mathematical	`Finset` `instHasSubset`	`Ico` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `image` `decidableEq` `instUnion` `ssubsets` `instSDiff`	—	`ext` `sdiff_lt_sdiff_right` `sup_sdiff_cancel_right` `le_sup_left` `sup_lt_of_lt_sdiff_left`
`Iic_eq_powerset` 📖	mathematical	—	`Iic` `Finset` `PartialOrder.toPreorder` `partialOrder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `powerset`	—	`ext`
`Iio_eq_ssubsets` 📖	mathematical	—	`Iio` `Finset` `PartialOrder.toPreorder` `partialOrder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `ssubsets`	—	`ext`
`Ioc_eq_filter_powerset` 📖	mathematical	—	`Ioc` `Finset` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `filter` `instHasSSubset` `instDecidableRelSSubset` `powerset`	—	`ext`
`Ioo_eq_filter_ssubsets` 📖	mathematical	—	`Ioo` `Finset` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `filter` `instHasSSubset` `instDecidableRelSSubset` `ssubsets`	—	`ext`
`antitone_iff_forall_cons_le` 📖	mathematical	—	`Antitone` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE` `cons`	—	`monotone_iff_forall_le_cons`
`antitone_iff_forall_insert_le` 📖	mathematical	—	`Antitone` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE` `instInsert`	—	`monotone_iff_forall_le_insert`
`card_Icc_finset` 📖	mathematical	`Finset` `instHasSubset`	`card` `Icc` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`disjUnion_eq_union` `card_map` `card_attach` `card_powerset` `card_sdiff_of_subset`
`card_Ico_finset` 📖	mathematical	`Finset` `instHasSubset`	`card` `Ico` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`card_Ico_eq_card_Icc_sub_one` `card_Icc_finset`
`card_Iic_finset` 📖	mathematical	—	`card` `Finset` `Iic` `PartialOrder.toPreorder` `partialOrder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`Iic_eq_powerset` `card_powerset`
`card_Iio_finset` 📖	mathematical	—	`card` `Finset` `Iio` `PartialOrder.toPreorder` `partialOrder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`Iio_eq_ssubsets` `ssubsets.eq_1` `card_erase_of_mem` `mem_powerset_self` `card_powerset`
`card_Ioc_finset` 📖	mathematical	`Finset` `instHasSubset`	`card` `Ioc` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`card_Ioc_eq_card_Icc_sub_one` `card_Icc_finset`
`card_Ioo_finset` 📖	mathematical	`Finset` `instHasSubset`	`card` `Ioo` `PartialOrder.toPreorder` `partialOrder` `instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`card_Ioo_eq_card_Icc_sub_two` `card_Icc_finset`
`monotone_iff_forall_le_cons` 📖	mathematical	—	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE` `cons`	—	`cons_eq_insert`
`monotone_iff_forall_le_insert` 📖	mathematical	—	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE` `instInsert`	—	`cons_eq_insert`
`strictAnti_iff_forall_cons_lt` 📖	mathematical	—	`StrictAnti` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT` `cons`	—	`strictMono_iff_forall_lt_cons`
`strictAnti_iff_forall_lt_insert` 📖	mathematical	—	`StrictAnti` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT` `instInsert`	—	`strictMono_iff_forall_lt_insert`
`strictMono_iff_forall_lt_cons` 📖	mathematical	—	`StrictMono` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT` `cons`	—	`cons_eq_insert`
`strictMono_iff_forall_lt_insert` 📖	mathematical	—	`StrictMono` `Finset` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT` `instInsert`	—	`cons_eq_insert`

---

← Back to Index