Sum

📁 Source: Mathlib/Data/Finset/Sum.lean

Statistics

Metric	Count
Definitions disjSum, sumEquiv, toLeft, toRight	4
Theorems Injective2_disjSum, card_disjSum, card_toLeft_add_card_toRight, card_toLeft_le, card_toRight_le, disjSum_empty, disjSum_eq_empty, disjSum_eq_iff, disjSum_inj, disjSum_mono, disjSum_mono_left, disjSum_mono_right, disjSum_ssubset_disjSum_of_ssubset_of_subset, disjSum_ssubset_disjSum_of_subset_of_ssubset, disjSum_strictMono_left, disjSum_strictMono_right, disjSum_subset, disjoint_map_inl_map_inr, empty_disjSum, eq_disjSum_iff, fold_disjSum, gc_map_inl_toLeft, gc_map_inr_toRight, inl_mem_disjSum, inr_mem_disjSum, map_disjSum, map_inl_disjUnion_map_inr, map_inl_subset_iff_subset_toLeft, map_inr_subset_iff_subset_toRight, mem_disjSum, mem_toLeft, mem_toRight, subset_disjSum, subset_map_inl, subset_map_inr, sumEquiv_apply_fst, sumEquiv_apply_snd, sumEquiv_symm_apply, toLeft_cons_inl, toLeft_cons_inr, toLeft_disjSum, toLeft_disjSum_toRight, toLeft_image_swap, toLeft_insert_inl, toLeft_insert_inr, toLeft_inter, toLeft_map_sumComm, toLeft_monotone, toLeft_sdiff, toLeft_subset_toLeft, toLeft_union, toRight_cons_inl, toRight_cons_inr, toRight_disjSum, toRight_image_swap, toRight_insert_inl, toRight_insert_inr, toRight_inter, toRight_map_sumComm, toRight_monotone, toRight_sdiff, toRight_subset_toRight, toRight_union, val_disjSum	64
Total	68

Finset

Definitions

Name	Category	Theorems
disjSum 📖	CompOp	46 math math: fold_disjSum, val_disjSum, univ_disjSum_univ, toRight_disjSum, Sum.Lex.Ioo_inl_inr, disjSum_subset, disjSum_empty, Sum.Lex.Iic_inr, Finsupp.sumElim_support, eq_disjSum_iff, disjSum_ssubset_disjSum_of_subset_of_ssubset, inr_mem_disjSum, disjSum_strictMono_left, Sum.Lex.Ici_inl, disjSum_mono, map_inl_disjUnion_map_inr, Sum.Lex.Ioc_inl_inr, disjSum_mono_right, disjSum_eq_empty, disjSum_inj, sum_disjSum, Sum.Lex.Ioi_inl, sum_sumElim, centerMass_segment', sup_disjSum, Sum.Lex.Ico_inl_inr, toLeft_disjSum, Sum.Lex.Iio_inr, mem_disjSum, Injective2_disjSum, prod_disjSum, inl_mem_disjSum, map_disjSum, card_disjSum, toLeft_disjSum_toRight, disjSum_mono_left, disjSum_ssubset_disjSum_of_ssubset_of_subset, disjSum_eq_iff, prod_sumElim, inf_disjSum, subset_disjSum, disjSum_strictMono_right, empty_disjSum, Sum.Lex.Icc_inl_inr, sumEquiv_symm_apply, sumLexLift_inl_inr
sumEquiv 📖	CompOp	3 math math: sumEquiv_apply_snd, sumEquiv_apply_fst, sumEquiv_symm_apply
toLeft 📖	CompOp	34 math math: toLeft_cons_inl, toLeft_monotone, toLeft_map_sumComm, toLeft_eq_univ, prod_sum_eq_prod_toLeft_mul_prod_toRight, sum_sum_eq_sum_toLeft_add_sum_toRight, disjSum_subset, card_toLeft_le, eq_disjSum_iff, toLeft_subset_toLeft, subset_map_inl, toLeft_image_swap, toRight_map_sumComm, toLeft_univ, toLeft_cons_inr, toLeft_sdiff, Filter.tendsto_toLeft_atTop, toLeft_eq_empty, toRight_image_swap, card_toLeft_add_card_toRight, mem_toLeft, map_inl_subset_iff_subset_toLeft, toLeft_disjSum, toLeft_disjSum_toRight, toLeft_insert_inr, subset_map_inr, disjSum_eq_iff, toLeft_union, sumEquiv_apply_fst, subset_disjSum, toLeft_insert_inl, gc_map_inl_toLeft, toLeft_inter, preimage_inl
toRight 📖	CompOp	34 math math: toLeft_map_sumComm, prod_sum_eq_prod_toLeft_mul_prod_toRight, sum_sum_eq_sum_toLeft_add_sum_toRight, toRight_disjSum, preimage_inr, disjSum_subset, eq_disjSum_iff, subset_map_inl, toLeft_image_swap, toRight_map_sumComm, gc_map_inr_toRight, toRight_univ, toRight_monotone, toRight_insert_inr, toRight_image_swap, toRight_eq_univ, toRight_cons_inl, card_toLeft_add_card_toRight, toRight_subset_toRight, map_inr_subset_iff_subset_toRight, toRight_eq_empty, sumEquiv_apply_snd, toRight_cons_inr, card_toRight_le, toLeft_disjSum_toRight, mem_toRight, subset_map_inr, disjSum_eq_iff, toRight_sdiff, subset_disjSum, toRight_insert_inl, Filter.tendsto_toRight_atTop, toRight_union, toRight_inter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Injective2_disjSum 📖	mathematical	—	Function.Injective2 Finset disjSum	—	—
card_disjSum 📖	mathematical	—	card disjSum	—	Multiset.card_disjSum
card_toLeft_add_card_toRight 📖	mathematical	—	card toLeft toRight	—	card_disjSum toLeft_disjSum_toRight
card_toLeft_le 📖	mathematical	—	card toLeft	—	LE.le.trans_eq card_toLeft_add_card_toRight
card_toRight_le 📖	mathematical	—	card toRight	—	LE.le.trans_eq card_toLeft_add_card_toRight
disjSum_empty 📖	mathematical	—	disjSum Finset instEmptyCollection map Function.Embedding.inl	—	Multiset.disjSum_zero
disjSum_eq_empty 📖	mathematical	—	disjSum Finset instEmptyCollection	—	—
disjSum_eq_iff 📖	mathematical	—	disjSum toLeft toRight	—	toLeft_disjSum toRight_disjSum toLeft_disjSum_toRight
disjSum_inj 📖	mathematical	—	disjSum	—	—
disjSum_mono 📖	mathematical	Finset instHasSubset	disjSum	—	val_le_iff Multiset.disjSum_mono
disjSum_mono_left 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder disjSum	—	disjSum_mono Subset.rfl
disjSum_mono_right 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder disjSum	—	disjSum_mono Subset.rfl
disjSum_ssubset_disjSum_of_ssubset_of_subset 📖	mathematical	Finset instHasSSubset instHasSubset	disjSum	—	val_lt_iff Multiset.disjSum_lt_disjSum_of_lt_of_le val_le_iff
disjSum_ssubset_disjSum_of_subset_of_ssubset 📖	mathematical	Finset instHasSubset instHasSSubset	disjSum	—	val_lt_iff Multiset.disjSum_lt_disjSum_of_le_of_lt val_le_iff
disjSum_strictMono_left 📖	mathematical	—	StrictMono Finset PartialOrder.toPreorder partialOrder disjSum	—	disjSum_ssubset_disjSum_of_ssubset_of_subset Subset.rfl
disjSum_strictMono_right 📖	mathematical	—	StrictMono Finset PartialOrder.toPreorder partialOrder disjSum	—	disjSum_ssubset_disjSum_of_subset_of_ssubset Subset.rfl
disjSum_subset 📖	mathematical	—	Finset instHasSubset disjSum toLeft toRight	—	—
disjoint_map_inl_map_inr 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot map Function.Embedding.inl Function.Embedding.inr	—	—
empty_disjSum 📖	mathematical	—	disjSum Finset instEmptyCollection map Function.Embedding.inr	—	Multiset.zero_disjSum
eq_disjSum_iff 📖	mathematical	—	disjSum toLeft toRight	—	toLeft_disjSum toRight_disjSum toLeft_disjSum_toRight
fold_disjSum 📖	mathematical	—	fold disjSum	—	Multiset.fold.congr_simp Multiset.map_disjSum Multiset.fold_add
gc_map_inl_toLeft 📖	mathematical	—	GaloisConnection Finset PartialOrder.toPreorder partialOrder map Function.Embedding.inl toLeft	—	map_inl_subset_iff_subset_toLeft
gc_map_inr_toRight 📖	mathematical	—	GaloisConnection Finset PartialOrder.toPreorder partialOrder map Function.Embedding.inr toRight	—	map_inr_subset_iff_subset_toRight
inl_mem_disjSum 📖	mathematical	—	Finset instMembership disjSum	—	Multiset.inl_mem_disjSum
inr_mem_disjSum 📖	mathematical	—	Finset instMembership disjSum	—	Multiset.inr_mem_disjSum
map_disjSum 📖	mathematical	—	map disjSum disjUnion Function.Embedding.trans Function.Embedding.inl Function.Embedding.inr	—	val_injective Multiset.map_disjSum
map_inl_disjUnion_map_inr 📖	mathematical	—	disjUnion map Function.Embedding.inl Function.Embedding.inr disjoint_map_inl_map_inr disjSum	—	disjoint_map_inl_map_inr
map_inl_subset_iff_subset_toLeft 📖	mathematical	—	Finset instHasSubset map Function.Embedding.inl toLeft	—	—
map_inr_subset_iff_subset_toRight 📖	mathematical	—	Finset instHasSubset map Function.Embedding.inr toRight	—	—
mem_disjSum 📖	mathematical	—	Finset instMembership disjSum	—	Multiset.mem_disjSum
mem_toLeft 📖	mathematical	—	Finset instMembership toLeft	—	—
mem_toRight 📖	mathematical	—	Finset instMembership toRight	—	—
subset_disjSum 📖	mathematical	—	Finset instHasSubset disjSum toLeft toRight	—	—
subset_map_inl 📖	mathematical	—	Finset instHasSubset map Function.Embedding.inl toLeft toRight instEmptyCollection	—	—
subset_map_inr 📖	mathematical	—	Finset instHasSubset map Function.Embedding.inr toLeft instEmptyCollection toRight	—	—
sumEquiv_apply_fst 📖	mathematical	—	Finset DFunLike.coe RelIso Preorder.toLE PartialOrder.toPreorder partialOrder Prod.instLE_mathlib RelIso.instFunLike sumEquiv toLeft	—	—
sumEquiv_apply_snd 📖	mathematical	—	Finset DFunLike.coe RelIso Preorder.toLE PartialOrder.toPreorder partialOrder Prod.instLE_mathlib RelIso.instFunLike sumEquiv toRight	—	—
sumEquiv_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso Finset Prod.instLE_mathlib Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderIso OrderIso.symm sumEquiv disjSum	—	—
toLeft_cons_inl 📖	mathematical	Finset instMembership	toLeft cons	—	ext
toLeft_cons_inr 📖	mathematical	Finset instMembership	toLeft cons	—	ext
toLeft_disjSum 📖	mathematical	—	toLeft disjSum	—	ext
toLeft_disjSum_toRight 📖	mathematical	—	disjSum toLeft toRight	—	ext
toLeft_image_swap 📖	mathematical	—	toLeft image toRight	—	ext
toLeft_insert_inl 📖	mathematical	—	toLeft Finset instInsert	—	ext
toLeft_insert_inr 📖	mathematical	—	toLeft Finset instInsert	—	ext
toLeft_inter 📖	mathematical	—	toLeft Finset instInter	—	ext
toLeft_map_sumComm 📖	mathematical	—	toLeft map Equiv.toEmbedding Equiv.sumComm toRight	—	ext
toLeft_monotone 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder toLeft	—	toLeft_subset_toLeft
toLeft_sdiff 📖	mathematical	—	toLeft Finset instSDiff	—	ext
toLeft_subset_toLeft 📖	mathematical	Finset instHasSubset	toLeft	—	—
toLeft_union 📖	mathematical	—	toLeft Finset instUnion	—	ext
toRight_cons_inl 📖	mathematical	Finset instMembership	toRight cons	—	ext
toRight_cons_inr 📖	mathematical	Finset instMembership	toRight cons	—	ext
toRight_disjSum 📖	mathematical	—	toRight disjSum	—	ext
toRight_image_swap 📖	mathematical	—	toRight image toLeft	—	ext
toRight_insert_inl 📖	mathematical	—	toRight Finset instInsert	—	ext
toRight_insert_inr 📖	mathematical	—	toRight Finset instInsert	—	ext
toRight_inter 📖	mathematical	—	toRight Finset instInter	—	ext
toRight_map_sumComm 📖	mathematical	—	toRight map Equiv.toEmbedding Equiv.sumComm toLeft	—	ext
toRight_monotone 📖	mathematical	—	Monotone Finset PartialOrder.toPreorder partialOrder toRight	—	toRight_subset_toRight
toRight_sdiff 📖	mathematical	—	toRight Finset instSDiff	—	ext
toRight_subset_toRight 📖	mathematical	Finset instHasSubset	toRight	—	—
toRight_union 📖	mathematical	—	toRight Finset instUnion	—	ext
val_disjSum 📖	mathematical	—	val disjSum Multiset.disjSum	—	—

---

← Back to Index