Indicator

📁 Source: Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems indicator_biUnion, indicator_biUnion_apply, indicator_sum, mulIndicator_biUnion, mulIndicator_biUnion_apply, mulIndicator_prod, prod_mulIndicator_eq_prod_filter, prod_mulIndicator_eq_prod_inter, prod_mulIndicator_subset, prod_mulIndicator_subset_of_eq_one, sum_indicator_eq_sum_filter, sum_indicator_eq_sum_inter, sum_indicator_subset, sum_indicator_subset_of_eq_zero	14
Total	14

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indicator_biUnion 📖	mathematical	Set.PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset instSetLike	Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.iUnion instMembership sum	—	cons_induction Set.iUnion_congr_Prop notMem_empty Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.indicator_empty sum_cons cons_eq_insert set_biUnion_insert Set.indicator_union_of_notMem_inter Set.disjoint_iff Set.disjoint_iUnion₂_right Set.pairwiseDisjoint_insert_of_notMem Iff.not mem_coe coe_cons
indicator_biUnion_apply 📖	mathematical	Set.PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset instSetLike	Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.iUnion instMembership sum	—	indicator_biUnion
indicator_sum 📖	mathematical	—	Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Pi.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
mulIndicator_biUnion 📖	mathematical	Set.PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset instSetLike	Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Set.iUnion instMembership prod	—	cons_induction Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.mulIndicator_empty prod_cons cons_eq_insert set_biUnion_insert Set.mulIndicator_union_of_notMem_inter Set.disjoint_iff Set.disjoint_iUnion₂_right Set.pairwiseDisjoint_insert_of_notMem Iff.not mem_coe coe_cons
mulIndicator_biUnion_apply 📖	mathematical	Set.PairwiseDisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset instSetLike	Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Set.iUnion instMembership prod	—	mulIndicator_biUnion
mulIndicator_prod 📖	mathematical	—	Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Pi.commMonoid	—	map_prod MonoidHom.instMonoidHomClass
prod_mulIndicator_eq_prod_filter 📖	mathematical	—	prod Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid filter Set Set.instMembership	—	prod_filter_mul_prod_filter_not prod_congr Set.mulIndicator_of_mem mem_filter prod_eq_one Set.mulIndicator_of_notMem mul_one
prod_mulIndicator_eq_prod_inter 📖	mathematical	—	prod Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid SetLike.coe Finset instSetLike instInter	—	filter_mem_eq_inter prod_mulIndicator_eq_prod_filter
prod_mulIndicator_subset 📖	mathematical	Finset instHasSubset	prod Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid SetLike.coe instSetLike	—	prod_mulIndicator_subset_of_eq_one
prod_mulIndicator_subset_of_eq_one 📖	mathematical	Finset instHasSubset MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	prod Set.mulIndicator SetLike.coe instSetLike	—	prod_subset Set.mulIndicator_of_notMem prod_congr Set.mulIndicator_of_mem
sum_indicator_eq_sum_filter 📖	mathematical	—	sum Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid filter Set Set.instMembership	—	sum_filter_add_sum_filter_not sum_congr Set.indicator_of_mem mem_filter sum_eq_zero Set.indicator_of_notMem add_zero
sum_indicator_eq_sum_inter 📖	mathematical	—	sum Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.coe Finset instSetLike instInter	—	filter_mem_eq_inter sum_indicator_eq_sum_filter
sum_indicator_subset 📖	mathematical	Finset instHasSubset	sum Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.coe instSetLike	—	sum_indicator_subset_of_eq_zero
sum_indicator_subset_of_eq_zero 📖	mathematical	Finset instHasSubset AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum Set.indicator SetLike.coe instSetLike	—	sum_subset Set.indicator_of_notMem SetLike.mem_coe sum_congr Set.indicator_of_mem

---

← Back to Index