Interval

📁 Source: Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_add_Icc_subset, Icc_add_Ico_subset, Icc_mul_Icc_subset', Icc_mul_Ico_subset', Ici_add_Ici_subset, Ici_add_Ioi_subset, Ici_mul_Ici_subset', Ici_mul_Ioi_subset', Ico_add_Icc_subset, Ico_add_Ioc_subset, Ico_mul_Icc_subset', Ico_mul_Ioc_subset', Iic_add_Iic_subset, Iic_add_Iio_subset, Iic_mul_Iic_subset', Iic_mul_Iio_subset', Iio_add_Iic_subset, Iio_mul_Iic_subset', Ioc_add_Ico_subset, Ioc_mul_Ico_subset', Ioi_add_Ici_subset, Ioi_mul_Ici_subset'	22
Total	22

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_add_Icc_subset 📖	mathematical	—	Finset instHasSubset add Icc	—	coe_subset coe_add coe_Icc Set.Icc_add_Icc_subset
Icc_add_Ico_subset 📖	mathematical	—	Finset instHasSubset add Icc PartialOrder.toPreorder Ico	—	coe_subset coe_add coe_Icc coe_Ico Set.Icc_add_Ico_subset
Icc_mul_Icc_subset' 📖	mathematical	—	Finset instHasSubset mul Icc	—	coe_subset coe_mul coe_Icc Set.Icc_mul_Icc_subset'
Icc_mul_Ico_subset' 📖	mathematical	—	Finset instHasSubset mul Icc PartialOrder.toPreorder Ico	—	coe_subset coe_mul coe_Icc coe_Ico Set.Icc_mul_Ico_subset'
Ici_add_Ici_subset 📖	mathematical	—	Finset instHasSubset add Ici	—	coe_subset coe_add coe_Ici Set.Ici_add_Ici_subset
Ici_add_Ioi_subset 📖	mathematical	—	Finset instHasSubset add Ici PartialOrder.toPreorder Ioi	—	coe_subset coe_add coe_Ici coe_Ioi Set.Ici_add_Ioi_subset
Ici_mul_Ici_subset' 📖	mathematical	—	Finset instHasSubset mul Ici	—	coe_subset coe_mul coe_Ici Set.Ici_mul_Ici_subset'
Ici_mul_Ioi_subset' 📖	mathematical	—	Finset instHasSubset mul Ici PartialOrder.toPreorder Ioi	—	coe_subset coe_mul coe_Ici coe_Ioi Set.Ici_mul_Ioi_subset'
Ico_add_Icc_subset 📖	mathematical	—	Finset instHasSubset add Ico PartialOrder.toPreorder Icc	—	coe_subset coe_add coe_Ico coe_Icc Set.Ico_add_Icc_subset
Ico_add_Ioc_subset 📖	mathematical	—	Finset instHasSubset add Ico PartialOrder.toPreorder Ioc Ioo	—	coe_subset coe_add coe_Ico coe_Ioc coe_Ioo Set.Ico_add_Ioc_subset
Ico_mul_Icc_subset' 📖	mathematical	—	Finset instHasSubset mul Ico PartialOrder.toPreorder Icc	—	coe_subset coe_mul coe_Ico coe_Icc Set.Ico_mul_Icc_subset'
Ico_mul_Ioc_subset' 📖	mathematical	—	Finset instHasSubset mul Ico PartialOrder.toPreorder Ioc Ioo	—	coe_subset coe_mul coe_Ico coe_Ioc coe_Ioo Set.Ico_mul_Ioc_subset'
Iic_add_Iic_subset 📖	mathematical	—	Finset instHasSubset add Iic	—	coe_subset coe_add coe_Iic Set.Iic_add_Iic_subset
Iic_add_Iio_subset 📖	mathematical	—	Finset instHasSubset add Iic PartialOrder.toPreorder Iio	—	coe_subset coe_add coe_Iic coe_Iio Set.Iic_add_Iio_subset
Iic_mul_Iic_subset' 📖	mathematical	—	Finset instHasSubset mul Iic	—	coe_subset coe_mul coe_Iic Set.Iic_mul_Iic_subset'
Iic_mul_Iio_subset' 📖	mathematical	—	Finset instHasSubset mul Iic PartialOrder.toPreorder Iio	—	coe_subset coe_mul coe_Iic coe_Iio Set.Iic_mul_Iio_subset'
Iio_add_Iic_subset 📖	mathematical	—	Finset instHasSubset add Iio PartialOrder.toPreorder Iic	—	coe_subset coe_add coe_Iio coe_Iic Set.Iio_add_Iic_subset
Iio_mul_Iic_subset' 📖	mathematical	—	Finset instHasSubset mul Iio PartialOrder.toPreorder Iic	—	coe_subset coe_mul coe_Iio coe_Iic Set.Iio_mul_Iic_subset'
Ioc_add_Ico_subset 📖	mathematical	—	Finset instHasSubset add Ioc PartialOrder.toPreorder Ico Ioo	—	coe_subset coe_add coe_Ioc coe_Ico coe_Ioo Set.Ioc_add_Ico_subset
Ioc_mul_Ico_subset' 📖	mathematical	—	Finset instHasSubset mul Ioc PartialOrder.toPreorder Ico Ioo	—	coe_subset coe_mul coe_Ioc coe_Ico coe_Ioo Set.Ioc_mul_Ico_subset'
Ioi_add_Ici_subset 📖	mathematical	—	Finset instHasSubset add Ioi PartialOrder.toPreorder Ici	—	coe_subset coe_add coe_Ioi coe_Ici Set.Ioi_add_Ici_subset
Ioi_mul_Ici_subset' 📖	mathematical	—	Finset instHasSubset mul Ioi PartialOrder.toPreorder Ici	—	coe_subset coe_mul coe_Ioi coe_Ici Set.Ioi_mul_Ici_subset'

---

← Back to Index