Piecewise

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

Statistics

Metric	Count
Definitions	0
Theorems card_filter, dvd_prod_of_mem, prod_apply_dite, prod_apply_ite, prod_apply_ite_of_false, prod_apply_ite_of_true, prod_attach_eq_prod_dite, prod_dite, prod_dite_eq, prod_dite_eq', prod_dite_of_false, prod_dite_of_true, prod_eq_mul_prod_diff_singleton, prod_eq_prod_diff_singleton_mul, prod_eq_prod_iff_single, prod_inter_mul_prod_diff, prod_ite, prod_ite_eq, prod_ite_eq', prod_ite_eq_of_mem, prod_ite_eq_of_mem', prod_ite_mem, prod_ite_of_false, prod_ite_of_true, prod_ite_one, prod_pi_mulSingle, prod_pi_mulSingle', prod_piecewise, prod_pow_boole, prod_update_of_mem, prod_update_of_notMem, sum_apply_dite, sum_apply_ite, sum_apply_ite_of_false, sum_apply_ite_of_true, sum_attach_eq_sum_dite, sum_boole_nsmul, sum_dite, sum_dite_eq, sum_dite_eq', sum_dite_of_false, sum_dite_of_true, sum_eq_add_sum_diff_singleton, sum_eq_sum_diff_singleton_add, sum_eq_sum_iff_single, sum_inter_add_sum_diff, sum_ite, sum_ite_eq, sum_ite_eq', sum_ite_eq_of_mem, sum_ite_eq_of_mem', sum_ite_mem, sum_ite_of_false, sum_ite_of_true, sum_ite_zero, sum_pi_single, sum_pi_single', sum_piecewise, sum_update_of_mem, sum_update_of_notMem, prod_dite_eq, prod_dite_eq', prod_eq_mul_prod_compl, prod_eq_prod_compl_mul, prod_ite_eq, prod_ite_eq', prod_ite_eq_ite_exists, prod_ite_mem, prod_pi_mulSingle, prod_pi_mulSingle', sum_dite_eq, sum_dite_eq', sum_eq_add_sum_compl, sum_eq_sum_compl_add, sum_ite_eq, sum_ite_eq', sum_ite_eq_ite_exists, sum_ite_mem, sum_pi_single, sum_pi_single'	80
Total	80

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_filter 📖	mathematical	—	card filter sum Nat.instAddCommMonoid	—	sum_ite sum_const mul_one sum_const_zero add_zero
dvd_prod_of_mem 📖	mathematical	Finset instMembership	semigroupDvd Monoid.toSemigroup CommMonoid.toMonoid prod	—	prod_eq_mul_prod_diff_singleton dvd_mul_right
prod_apply_dite 📖	mathematical	—	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike filter univ Subtype.fintype	—	mem_filter prod_filter_mul_prod_filter_not prod_attach prod_congr
prod_apply_ite 📖	mathematical	—	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid filter	—	prod_apply_dite prod_attach
prod_apply_ite_of_false 📖	mathematical	—	prod	—	prod_congr prod_ite_of_false
prod_apply_ite_of_true 📖	mathematical	—	prod	—	prod_congr prod_ite_of_true
prod_attach_eq_prod_dite 📖	mathematical	—	prod Finset instMembership attach univ SetLike.instMembership instSetLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_dite univ_eq_attach prod_const_one mul_one ext Function.hfunext
prod_dite 📖	mathematical	—	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset SetLike.instMembership instSetLike filter univ Subtype.fintype	—	prod_apply_dite
prod_dite_eq 📖	mathematical	—	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_eq_single instIsEmptyFalse prod_eq_one
prod_dite_eq' 📖	mathematical	—	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_eq_single instIsEmptyFalse prod_eq_one
prod_dite_of_false 📖	mathematical	—	prod Finset SetLike.instMembership instSetLike univ Subtype.fintype	—	prod_bij' Subtype.coe_eta
prod_dite_of_true 📖	mathematical	—	prod Finset SetLike.instMembership instSetLike univ Subtype.fintype	—	prod_bij'
prod_eq_mul_prod_diff_singleton 📖	mathematical	Finset instMembership	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instSDiff instSingleton	—	prod_congr inter_singleton_of_mem prod_singleton prod_inter_mul_prod_diff
prod_eq_prod_diff_singleton_mul 📖	mathematical	Finset instMembership	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instSDiff instSingleton	—	prod_eq_mul_prod_diff_singleton mul_comm
prod_eq_prod_iff_single 📖	mathematical	Finset instMembership	prod	—	prod_eq_mul_prod_diff_singleton prod_congr
prod_inter_mul_prod_diff 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod Finset instInter instSDiff	—	prod_congr prod_piecewise
prod_ite 📖	mathematical	—	prod MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid filter	—	prod_apply_ite
prod_ite_eq 📖	mathematical	—	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_dite_eq
prod_ite_eq' 📖	mathematical	—	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_dite_eq'
prod_ite_eq_of_mem 📖	mathematical	Finset instMembership	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_ite_eq
prod_ite_eq_of_mem' 📖	mathematical	Finset instMembership	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_ite_eq'
prod_ite_mem 📖	mathematical	—	prod Finset instMembership decidableMem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instInter	—	prod_filter filter_mem_eq_inter
prod_ite_of_false 📖	mathematical	—	prod	—	prod_dite_of_false prod_attach
prod_ite_of_true 📖	mathematical	—	prod	—	prod_dite_of_true prod_attach
prod_ite_one 📖	mathematical	—	prod MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableExistsAndFinset	—	prod_eq_single_of_mem prod_eq_one Mathlib.Tactic.Push.not_and_eq
prod_pi_mulSingle 📖	mathematical	—	prod Pi.mulSingle MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_dite_eq
prod_pi_mulSingle' 📖	mathematical	—	prod Pi.mulSingle MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instMembership decidableMem	—	prod_dite_eq'
prod_piecewise 📖	mathematical	—	prod piecewise decidableMem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset instInter instSDiff	—	prod_congr prod_ite filter_mem_eq_inter sdiff_eq_filter
prod_pow_boole 📖	mathematical	—	prod Monoid.toNatPow CommMonoid.toMonoid Finset instMembership decidableMem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	prod_congr pow_ite pow_one pow_zero prod_ite_eq
prod_update_of_mem 📖	mathematical	Finset instMembership	prod Function.update MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instSDiff instSingleton	—	update_eq_piecewise prod_piecewise prod_congr inter_singleton_of_mem prod_const card_singleton pow_one
prod_update_of_notMem 📖	mathematical	Finset instMembership	prod Function.update	—	prod_congr Function.update_of_ne
sum_apply_dite 📖	mathematical	—	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike filter univ Subtype.fintype	—	mem_filter sum_filter_add_sum_filter_not sum_attach sum_congr
sum_apply_ite 📖	mathematical	—	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid filter	—	sum_apply_dite sum_attach
sum_apply_ite_of_false 📖	mathematical	—	sum	—	sum_congr sum_ite_of_false
sum_apply_ite_of_true 📖	mathematical	—	sum	—	sum_congr sum_ite_of_true
sum_attach_eq_sum_dite 📖	mathematical	—	sum Finset instMembership attach univ SetLike.instMembership instSetLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_dite univ_eq_attach sum_const_zero add_zero mem_filter mem_univ ext Function.hfunext Subtype.heq_iff_coe_eq
sum_boole_nsmul 📖	mathematical	—	sum AddMonoid.toNatSMul AddCommMonoid.toAddMonoid Finset instMembership decidableMem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	sum_congr ite_smul one_nsmul zero_nsmul sum_ite_eq
sum_dite 📖	mathematical	—	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset SetLike.instMembership instSetLike filter univ Subtype.fintype	—	sum_apply_dite
sum_dite_eq 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_eq_single IsEmpty.forall_iff instIsEmptyFalse sum_eq_zero
sum_dite_eq' 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_eq_single IsEmpty.forall_iff instIsEmptyFalse sum_eq_zero
sum_dite_of_false 📖	mathematical	—	sum Finset SetLike.instMembership instSetLike univ Subtype.fintype	—	sum_bij' mem_attach SetLike.coe_mem Subtype.coe_eta
sum_dite_of_true 📖	mathematical	—	sum Finset SetLike.instMembership instSetLike univ Subtype.fintype	—	sum_bij'
sum_eq_add_sum_diff_singleton 📖	mathematical	Finset instMembership	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instSDiff instSingleton	—	sum_congr inter_singleton_of_mem sum_singleton sum_inter_add_sum_diff
sum_eq_sum_diff_singleton_add 📖	mathematical	Finset instMembership	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instSDiff instSingleton	—	sum_eq_add_sum_diff_singleton add_comm
sum_eq_sum_iff_single 📖	mathematical	Finset instMembership	sum	—	sum_eq_add_sum_diff_singleton sum_congr mem_sdiff mem_singleton
sum_inter_add_sum_diff 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum Finset instInter instSDiff	—	sum_congr sum_piecewise
sum_ite 📖	mathematical	—	sum AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid filter	—	sum_apply_ite
sum_ite_eq 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_dite_eq
sum_ite_eq' 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_dite_eq'
sum_ite_eq_of_mem 📖	mathematical	Finset instMembership	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_ite_eq
sum_ite_eq_of_mem' 📖	mathematical	Finset instMembership	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_ite_eq'
sum_ite_mem 📖	mathematical	—	sum Finset instMembership decidableMem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instInter	—	sum_filter filter_mem_eq_inter
sum_ite_of_false 📖	mathematical	—	sum	—	sum_dite_of_false sum_attach
sum_ite_of_true 📖	mathematical	—	sum	—	sum_dite_of_true sum_attach
sum_ite_zero 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableExistsAndFinset	—	sum_eq_single_of_mem sum_eq_zero Mathlib.Tactic.Push.not_exists Mathlib.Tactic.Push.not_and_eq
sum_pi_single 📖	mathematical	—	sum Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_dite_eq
sum_pi_single' 📖	mathematical	—	sum Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instMembership decidableMem	—	sum_dite_eq'
sum_piecewise 📖	mathematical	—	sum piecewise decidableMem AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instInter instSDiff	—	sum_congr sum_ite filter_mem_eq_inter sdiff_eq_filter
sum_update_of_mem 📖	mathematical	Finset instMembership	sum Function.update AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instSDiff instSingleton	—	update_eq_piecewise sum_piecewise sum_congr inter_singleton_of_mem sum_const card_singleton one_nsmul
sum_update_of_notMem 📖	mathematical	Finset instMembership	sum Function.update	—	sum_congr Function.update_of_ne

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_dite_eq 📖	mathematical	—	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_dite_eq Finset.mem_univ
prod_dite_eq' 📖	mathematical	—	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_dite_eq' Finset.mem_univ
prod_eq_mul_prod_compl 📖	mathematical	—	Finset.prod Finset.univ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Finset.instSingleton	—	Finset.prod_eq_mul_prod_diff_singleton Finset.mem_univ
prod_eq_prod_compl_mul 📖	mathematical	—	Finset.prod Finset.univ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Finset.instSingleton	—	Finset.prod_eq_prod_diff_singleton_mul Finset.mem_univ
prod_ite_eq 📖	mathematical	—	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_ite_eq Finset.mem_univ
prod_ite_eq' 📖	mathematical	—	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_ite_eq' Finset.mem_univ
prod_ite_eq_ite_exists 📖	mathematical	—	Finset.prod Finset.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid decidableExistsFintype	—	Finset.prod_ite_one
prod_ite_mem 📖	mathematical	—	Finset.prod Finset.univ Finset Finset.instMembership Finset.decidableMem MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Finset.prod_ite_mem Finset.prod_congr Finset.univ_inter
prod_pi_mulSingle 📖	mathematical	—	Finset.prod Finset.univ Pi.mulSingle MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_dite_eq
prod_pi_mulSingle' 📖	mathematical	—	Finset.prod Finset.univ Pi.mulSingle MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_dite_eq'
sum_dite_eq 📖	mathematical	—	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_dite_eq Finset.mem_univ
sum_dite_eq' 📖	mathematical	—	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_dite_eq' Finset.mem_univ
sum_eq_add_sum_compl 📖	mathematical	—	Finset.sum Finset.univ AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Finset.instSingleton	—	Finset.sum_eq_add_sum_diff_singleton Finset.mem_univ
sum_eq_sum_compl_add 📖	mathematical	—	Finset.sum Finset.univ AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Compl.compl Finset BooleanAlgebra.toCompl Finset.booleanAlgebra Finset.instSingleton	—	Finset.sum_eq_sum_diff_singleton_add Finset.mem_univ
sum_ite_eq 📖	mathematical	—	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_ite_eq Finset.mem_univ
sum_ite_eq' 📖	mathematical	—	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_ite_eq' Finset.mem_univ
sum_ite_eq_ite_exists 📖	mathematical	—	Finset.sum Finset.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid decidableExistsFintype	—	Finset.sum_ite_zero Finset.mem_univ
sum_ite_mem 📖	mathematical	—	Finset.sum Finset.univ Finset Finset.instMembership Finset.decidableMem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_ite_mem Finset.sum_congr Finset.univ_inter
sum_pi_single 📖	mathematical	—	Finset.sum Finset.univ Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_dite_eq
sum_pi_single' 📖	mathematical	—	Finset.sum Finset.univ Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_dite_eq'

---

← Back to Index