LocallyFinite

📁 Source: Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean

Statistics

Metric	Count
Definitions	0
Theorems add_sum_Ico_eq_sum_Icc, add_sum_Iio_eq_sum_Iic, add_sum_Ioc_eq_sum_Icc, add_sum_Ioi_eq_sum_Ici, add_sum_Ioo_eq_sum_Ico, add_sum_Ioo_eq_sum_Ioc, mul_prod_Ico_eq_prod_Icc, mul_prod_Iio_eq_prod_Iic, mul_prod_Ioc_eq_prod_Icc, mul_prod_Ioi_eq_prod_Ici, mul_prod_Ioo_eq_prod_Ico, mul_prod_Ioo_eq_prod_Ioc, prod_Ico_mul_eq_prod_Icc, prod_Ico_mul_eq_prod_Ico_add_one, prod_Iio_mul_eq_prod_Iic, prod_Ioc_mul_eq_prod_Icc, prod_Ioi_mul_eq_prod_Ici, prod_Ioo_mul_eq_prod_Ico, prod_Ioo_mul_eq_prod_Ioc, prod_eq_prod_Ico_succ_bot, prod_eq_prod_range_sdiff, prod_prod_Ioi_mul_eq_prod_prod_off_diag, sum_Ico_add_eq_sum_Icc, sum_Ico_add_eq_sum_Ico_add_one, sum_Iio_add_eq_sum_Iic, sum_Ioc_add_eq_sum_Icc, sum_Ioi_add_eq_sum_Ici, sum_Ioo_add_eq_sum_Ico, sum_Ioo_add_eq_sum_Ioc, sum_eq_sum_Ico_succ_bot, sum_eq_sum_range_sdiff, sum_sum_Ioi_add_eq_sum_sum_off_diag	32
Total	32

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_sum_Ico_eq_sum_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ico Icc	—	right_notMem_Ico Icc_eq_cons_Ico sum_cons
add_sum_Iio_eq_sum_Iic 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Iio PartialOrder.toPreorder Iic	—	notMem_Iio_self Iic_eq_cons_Iio sum_cons
add_sum_Ioc_eq_sum_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioc Icc	—	left_notMem_Ioc Icc_eq_cons_Ioc sum_cons
add_sum_Ioi_eq_sum_Ici 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioi PartialOrder.toPreorder Ici	—	notMem_Ioi_self Ici_eq_cons_Ioi sum_cons
add_sum_Ioo_eq_sum_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioo Ico	—	left_notMem_Ioo Ico_eq_cons_Ioo sum_cons
add_sum_Ioo_eq_sum_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioo Ioc	—	right_notMem_Ioo Ioc_eq_cons_Ioo sum_cons
mul_prod_Ico_eq_prod_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ico Icc	—	right_notMem_Ico Icc_eq_cons_Ico prod_cons
mul_prod_Iio_eq_prod_Iic 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Iio PartialOrder.toPreorder Iic	—	notMem_Iio_self Iic_eq_cons_Iio prod_cons
mul_prod_Ioc_eq_prod_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioc Icc	—	left_notMem_Ioc Icc_eq_cons_Ioc prod_cons
mul_prod_Ioi_eq_prod_Ici 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioi PartialOrder.toPreorder Ici	—	notMem_Ioi_self Ici_eq_cons_Ioi prod_cons
mul_prod_Ioo_eq_prod_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioo Ico	—	left_notMem_Ioo Ico_eq_cons_Ioo prod_cons
mul_prod_Ioo_eq_prod_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioo Ioc	—	right_notMem_Ioo Ioc_eq_cons_Ioo prod_cons
prod_Ico_mul_eq_prod_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ico Icc	—	mul_comm mul_prod_Ico_eq_prod_Icc
prod_Ico_mul_eq_prod_Ico_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ico AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne	—	insert_Ico_right_eq_Ico_add_one prod_insert right_notMem_Ico mul_comm
prod_Iio_mul_eq_prod_Iic 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Iio PartialOrder.toPreorder Iic	—	mul_comm mul_prod_Iio_eq_prod_Iic
prod_Ioc_mul_eq_prod_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioc Icc	—	mul_comm mul_prod_Ioc_eq_prod_Icc
prod_Ioi_mul_eq_prod_Ici 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioi PartialOrder.toPreorder Ici	—	mul_comm mul_prod_Ioi_eq_prod_Ici
prod_Ioo_mul_eq_prod_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioo Ico	—	mul_comm mul_prod_Ioo_eq_prod_Ico
prod_Ioo_mul_eq_prod_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Ioo Ioc	—	mul_comm mul_prod_Ioo_eq_prod_Ioc
prod_eq_prod_Ico_succ_bot 📖	mathematical	—	prod Ico Nat.instPreorder Nat.instLocallyFiniteOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd prod_insert insert_Ico_add_one_left_eq_Ico
prod_eq_prod_range_sdiff 📖	mathematical	Monotone Finset Nat.instPreorder PartialOrder.toPreorder partialOrder	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid range instSDiff	—	Monotone.partialSups_eq Pairwise.set_pairwise disjoint_disjointed disjiUnion_Iic_disjointed Iic_eq_Icc prod_disjiUnion Nat.bot_eq_zero Nat.range_succ_eq_Icc_zero prod_range_succ' mul_comm disjointed_zero comp_sup_eq_sup_comp_of_nonempty nonempty_Iic sup_Iic
prod_prod_Ioi_mul_eq_prod_prod_off_diag 📖	mathematical	—	prod univ Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra LinearOrder.toDecidableEq instSingleton	—	disjoint_Ioi_Iio prod_congr prod_disjUnion prod_mul_distrib prod_sigma' prod_nbij' Sigma.eta
sum_Ico_add_eq_sum_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ico Icc	—	add_comm add_sum_Ico_eq_sum_Icc
sum_Ico_add_eq_sum_Ico_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ico AddSemigroup.toAdd AddMonoid.toAddSemigroup AddMonoidWithOne.toAddMonoid AddMonoidWithOne.toOne	—	insert_Ico_right_eq_Ico_add_one sum_insert right_notMem_Ico add_comm
sum_Iio_add_eq_sum_Iic 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Iio PartialOrder.toPreorder Iic	—	add_comm add_sum_Iio_eq_sum_Iic
sum_Ioc_add_eq_sum_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioc Icc	—	add_comm add_sum_Ioc_eq_sum_Icc
sum_Ioi_add_eq_sum_Ici 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioi PartialOrder.toPreorder Ici	—	add_comm add_sum_Ioi_eq_sum_Ici
sum_Ioo_add_eq_sum_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioo Ico	—	add_comm add_sum_Ioo_eq_sum_Ico
sum_Ioo_add_eq_sum_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Ioo Ioc	—	add_comm add_sum_Ioo_eq_sum_Ioc
sum_eq_sum_Ico_succ_bot 📖	mathematical	—	sum Ico Nat.instPreorder Nat.instLocallyFiniteOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	mem_Ico add_le_iff_nonpos_right IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le nonpos_iff_eq_zero Nat.instCanonicallyOrderedAdd one_ne_zero sum_insert insert_Ico_add_one_left_eq_Ico
sum_eq_sum_range_sdiff 📖	mathematical	Monotone Finset Nat.instPreorder PartialOrder.toPreorder partialOrder	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid range instSDiff	—	Monotone.partialSups_eq Pairwise.set_pairwise disjoint_disjointed disjiUnion_Iic_disjointed Iic_eq_Icc sum_disjiUnion Nat.bot_eq_zero Nat.range_succ_eq_Icc_zero sum_range_succ' add_comm disjointed_zero comp_sup_eq_sup_comp_of_nonempty nonempty_Iic sup_Iic
sum_sum_Ioi_add_eq_sum_sum_off_diag 📖	mathematical	—	sum univ Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Compl.compl Finset BooleanAlgebra.toCompl booleanAlgebra LinearOrder.toDecidableEq instSingleton	—	disjoint_Ioi_Iio sum_congr Ioi_disjUnion_Iio sum_disjUnion sum_add_distrib sum_sigma' sum_nbij' mem_sigma mem_univ mem_Ioi mem_Iio Sigma.eta

---

← Back to Index