Interval

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

Statistics

Metric	Count
Definitions instLocallyFiniteOrder, rangeIcc, rangeSingleton	3
Theorems Icc_eq, card_Icc, card_Ico, card_Iic, card_Iio, card_Ioc, card_Ioo, card_uIcc, coe_rangeIcc, mem_rangeIcc_apply_iff, mem_rangeSingleton_apply_iff, rangeIcc_apply, rangeIcc_support, rangeIcc_toFun, rangeSingleton_apply, rangeSingleton_support	16
Total	19

Finsupp

Definitions

Name	Category	Theorems
instLocallyFiniteOrder 📖	CompOp	14 math math: card_Ioc, card_Ico, Nat.properDivisors_eq_image_Iio_factorization_prod_pow, card_Icc, card_uIcc, card_Ioo, Nat.divisors_eq_map_attach_Iic_factorization_prod_pow, Nat.Iio_factorization_prod_pow_injective, card_Iic, card_Iio, Icc_eq, Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow, Nat.Iic_factorization_prod_pow_injective, Nat.divisors_eq_image_Iic_factorization_prod_pow
rangeIcc 📖	CompOp	6 math math: rangeIcc_toFun, rangeIcc_apply, mem_rangeIcc_apply_iff, coe_rangeIcc, Icc_eq, rangeIcc_support
rangeSingleton 📖	CompOp	3 math math: rangeSingleton_support, mem_rangeSingleton_apply_iff, rangeSingleton_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_eq 📖	mathematical	—	Finset.Icc Finsupp preorder PartialOrder.toPreorder instLocallyFiniteOrder Finset.finsupp Finset Finset.instUnion support DFunLike.coe Finset.zero instFunLike rangeIcc	—	—
card_Icc 📖	mathematical	—	Finset.card Finsupp Finset.Icc preorder PartialOrder.toPreorder instLocallyFiniteOrder Finset.prod Nat.instCommMonoid Finset Finset.instUnion support DFunLike.coe instFunLike	—	Finset.card_finsupp Finset.prod_congr
card_Ico 📖	mathematical	—	Finset.card Finsupp Finset.Ico preorder PartialOrder.toPreorder instLocallyFiniteOrder Finset.prod Nat.instCommMonoid Finset Finset.instUnion support Finset.Icc DFunLike.coe instFunLike	—	Finset.card_Ico_eq_card_Icc_sub_one card_Icc
card_Iic 📖	mathematical	—	Finset.card Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.Iic preorder PartialOrder.toPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot orderBot instLocallyFiniteOrder Finset.prod Nat.instCommMonoid support DFunLike.coe instFunLike	—	Finset.prod_congr card_Icc Finset.empty_union bot_eq_zero
card_Iio 📖	mathematical	—	Finset.card Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.Iio preorder PartialOrder.toPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot orderBot instLocallyFiniteOrder Finset.prod Nat.instCommMonoid support Finset.Iic DFunLike.coe instFunLike	—	Finset.card_Iio_eq_card_Iic_sub_one card_Iic
card_Ioc 📖	mathematical	—	Finset.card Finsupp Finset.Ioc preorder PartialOrder.toPreorder instLocallyFiniteOrder Finset.prod Nat.instCommMonoid Finset Finset.instUnion support Finset.Icc DFunLike.coe instFunLike	—	Finset.card_Ioc_eq_card_Icc_sub_one card_Icc
card_Ioo 📖	mathematical	—	Finset.card Finsupp Finset.Ioo preorder PartialOrder.toPreorder instLocallyFiniteOrder Finset.prod Nat.instCommMonoid Finset Finset.instUnion support Finset.Icc DFunLike.coe instFunLike	—	Finset.card_Ioo_eq_card_Icc_sub_two card_Icc
card_uIcc 📖	mathematical	—	Finset.card Finsupp Finset.uIcc lattice instLocallyFiniteOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Finset.prod Nat.instCommMonoid Finset Finset.instUnion support DFunLike.coe instFunLike	—	support_inf_union_support_sup card_Icc
coe_rangeIcc 📖	mathematical	—	DFunLike.coe Finsupp Finset Finset.zero instFunLike rangeIcc Finset.Icc PartialOrder.toPreorder	—	—
mem_rangeIcc_apply_iff 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike DFunLike.coe Finsupp Finset.zero instFunLike rangeIcc Preorder.toLE PartialOrder.toPreorder	—	Finset.mem_Icc
mem_rangeSingleton_apply_iff 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike DFunLike.coe Finsupp Finset.zero instFunLike rangeSingleton	—	Finset.mem_singleton
rangeIcc_apply 📖	mathematical	—	DFunLike.coe Finsupp Finset Finset.zero instFunLike rangeIcc Finset.Icc PartialOrder.toPreorder	—	—
rangeIcc_support 📖	mathematical	—	support Finset Finset.zero rangeIcc Finset.instUnion	—	—
rangeIcc_toFun 📖	mathematical	—	DFunLike.coe Finsupp Finset Finset.zero instFunLike rangeIcc Finset.Icc PartialOrder.toPreorder	—	rangeIcc_apply
rangeSingleton_apply 📖	mathematical	—	DFunLike.coe Finsupp Finset Finset.zero instFunLike rangeSingleton Finset.instSingleton	—	—
rangeSingleton_support 📖	mathematical	—	support Finset Finset.zero rangeSingleton	—	—

---

← Back to Index