Fold

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

Statistics

Metric	Count
Definitions `fold`	1
Theorems `fold_congr`, `fold_cons`, `fold_const`, `fold_disjUnion`, `fold_empty`, `fold_hom`, `fold_image`, `fold_image_idem`, `fold_insert`, `fold_insert_idem`, `fold_ite`, `fold_ite'`, `fold_map`, `fold_max_le`, `fold_max_lt`, `fold_min_le`, `fold_min_lt`, `fold_op_distrib`, `fold_op_rel_iff_and`, `fold_op_rel_iff_or`, `fold_singleton`, `fold_sup_bot_singleton`, `fold_union_empty_singleton`, `fold_union_inter`, `le_fold_max`, `le_fold_min`, `lt_fold_max`, `lt_fold_min`	28
Total	29

Finset

Definitions

Name	Category	Theorems
`fold` 📖	CompOp	36 math math: `fold_disjSum`, `le_fold_min`, `fold_const`, `le_fold_max`, `fold_min_lt`, `Polynomial.natDegree_sum_le`, `fold_image_idem`, `fold_cons`, `fold_singleton`, `lt_fold_min`, `fold_max_add`, `fold_disjUnion`, `sum_eq_fold`, `fold_congr`, `fold_ite'`, `fold_sup_univ`, `fold_union_empty_singleton`, `prod_eq_fold`, `fold_disjiUnion`, `fold_sup_bot_singleton`, `fold_empty`, `fold_max_le`, `fold_insert_idem`, `fold_min_le`, `fold_map`, `fold_ite`, `fold_image`, `fold_union_inter`, `fold_op_rel_iff_and`, `fold_max_lt`, `fold_op_distrib`, `lt_fold_max`, `fold_hom`, `fold_inf_univ`, `fold_insert`, `fold_op_rel_iff_or`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fold_congr` 📖	mathematical	—	`fold`	—	`fold.eq_1` `Multiset.map_congr`
`fold_cons` 📖	mathematical	`Finset` `instMembership`	`fold` `cons`	—	`cons_val` `Multiset.map_cons` `Multiset.fold_cons_left`
`fold_const` 📖	mathematical	—	`fold` `Finset` `instEmptyCollection`	—	`induction_on` `fold_insert`
`fold_disjUnion` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`fold` `disjUnion`	—	`Multiset.map_add` `Multiset.fold_add`
`fold_empty` 📖	mathematical	—	`fold` `Finset` `instEmptyCollection`	—	—
`fold_hom` 📖	mathematical	—	`fold`	—	`fold.eq_1` `Multiset.fold_hom` `Multiset.map_map` `Multiset.fold.congr_simp` `Multiset.map_congr`
`fold_image` 📖	mathematical	`Set.InjOn` `SetLike.coe` `Finset` `instSetLike`	`fold` `image`	—	`Multiset.fold.congr_simp` `Multiset.map_congr` `image_val_of_injOn` `Multiset.map_map`
`fold_image_idem` 📖	mathematical	—	`fold` `image`	—	`cons_induction` `fold_empty` `image_empty` `fold_cons` `cons_eq_insert` `image_insert` `fold_insert_idem` `fold_congr`
`fold_insert` 📖	mathematical	`Finset` `instMembership`	`fold` `instInsert`	—	`insert_val` `Multiset.ndinsert_of_notMem` `Multiset.map_cons` `Multiset.fold_cons_left`
`fold_insert_idem` 📖	mathematical	—	`fold` `Finset` `instInsert`	—	`insert_erase` `fold.congr_simp` `insert_eq_of_mem` `fold_insert`
`fold_ite` 📖	mathematical	—	`fold` `filter`	—	`fold_ite'`
`fold_ite'` 📖	mathematical	—	`fold` `filter`	—	`induction_on` `fold.congr_simp` `filter_empty` `fold_insert` `filter_insert`
`fold_map` 📖	mathematical	—	`fold` `map` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Multiset.fold.congr_simp` `Multiset.map_map`
`fold_max_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instCommutativeMax` `instAssociativeMax`	—	`instCommutativeMax` `instAssociativeMax` `fold_op_rel_iff_and` `max_le_iff`
`fold_max_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instCommutativeMax` `instAssociativeMax`	—	`instCommutativeMax` `instAssociativeMax` `fold_op_rel_iff_and` `max_lt_iff`
`fold_min_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeInf.toMin` `instCommutativeMin` `instAssociativeMin` `Finset` `instMembership`	—	`instCommutativeMin` `instAssociativeMin` `fold_op_rel_iff_or` `min_le_iff`
`fold_min_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeInf.toMin` `instCommutativeMin` `instAssociativeMin` `Finset` `instMembership`	—	`instCommutativeMin` `instAssociativeMin` `fold_op_rel_iff_or` `min_lt_iff`
`fold_op_distrib` 📖	mathematical	—	`fold`	—	`Multiset.fold_distrib`
`fold_op_rel_iff_and` 📖	mathematical	—	`fold`	—	`induction_on` `instIsEmptyFalse` `fold_insert`
`fold_op_rel_iff_or` 📖	mathematical	—	`fold` `Finset` `instMembership`	—	`induction_on` `fold_insert`
`fold_singleton` 📖	mathematical	—	`fold` `Finset` `instSingleton`	—	—
`fold_sup_bot_singleton` 📖	mathematical	—	`fold` `Finset` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instLattice` `instCommutativeMax_mathlib` `instAssociativeMax_mathlib` `Bot.bot` `GeneralizedBooleanAlgebra.toBot` `instGeneralizedBooleanAlgebra` `instSingleton`	—	`fold_union_empty_singleton`
`fold_union_empty_singleton` 📖	mathematical	—	`fold` `Finset` `instUnion` `instCommutativeUnion` `instAssociativeUnion` `instEmptyCollection` `instSingleton`	—	`induction_on` `instCommutativeUnion` `instAssociativeUnion` `fold_insert` `insert_eq`
`fold_union_inter` 📖	mathematical	—	`fold` `Finset` `instUnion` `instInter`	—	`Multiset.fold_add` `Multiset.map_add` `union_val` `inter_val` `Multiset.union_add_inter`
`le_fold_max` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instCommutativeMax` `instAssociativeMax` `Finset` `instMembership`	—	`fold_op_rel_iff_or` `instCommutativeMax` `instAssociativeMax` `le_max_iff`
`le_fold_min` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeInf.toMin` `instCommutativeMin` `instAssociativeMin`	—	`fold_op_rel_iff_and` `instCommutativeMin` `instAssociativeMin` `le_min_iff`
`lt_fold_max` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `instCommutativeMax` `instAssociativeMax` `Finset` `instMembership`	—	`fold_op_rel_iff_or` `instCommutativeMax` `instAssociativeMax` `lt_max_iff`
`lt_fold_min` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `fold` `SemilatticeInf.toMin` `instCommutativeMin` `instAssociativeMin`	—	`fold_op_rel_iff_and` `instCommutativeMin` `instAssociativeMin` `lt_min_iff`

---

← Back to Index