Composition

📁 Source: Mathlib/Combinatorics/Enumerative/Composition.lean

Statistics

Metric	Count
Definitions `append`, `blocks`, `blocksFinEquiv`, `blocksFun`, `boundaries`, `boundary`, `cast`, `embedding`, `index`, `instInhabited`, `instToString`, `invEmbedding`, `length`, `ones`, `recOnAppendSingle`, `recOnSingleAppend`, `reverse`, `single`, `sizeUpTo`, `toCompositionAsSet`, `CompositionAsSet`, `blocks`, `blocksFun`, `boundaries`, `boundary`, `length`, `toComposition`, `splitWrtComposition`, `splitWrtCompositionAux`, `compositionAsSetEquiv`, `compositionAsSetFintype`, `compositionEquiv`, `compositionFintype`, `instDecidableEqComposition`, `decEq`, `instDecidableEqCompositionAsSet`, `decEq`, `instInhabitedCompositionAsSet`	38
Theorems `append_blocks`, `blocksFun_congr`, `blocksFun_le`, `blocksFun_mem_blocks`, `blocks_eq_nil`, `blocks_le`, `blocks_length`, `blocks_pos`, `blocks_pos'`, `blocks_sum`, `boundary_last`, `boundary_zero`, `card_boundaries_eq_succ_length`, `cast_blocks`, `cast_eq_cast`, `cast_heq`, `cast_rfl`, `coe_embedding`, `coe_invEmbedding`, `disjoint_range`, `embedding_comp_inv`, `eq_ones_iff`, `eq_ones_iff_le_length`, `eq_ones_iff_length`, `eq_single_iff_length`, `ext`, `ext_iff`, `index_embedding`, `index_exists`, `invEmbedding_comp`, `length_eq_zero`, `length_le`, `length_pos_iff`, `length_pos_of_pos`, `lt_sizeUpTo_index_succ`, `mem_range_embedding`, `mem_range_embedding_iff`, `mem_range_embedding_iff'`, `monotone_sizeUpTo`, `ne_ones_iff`, `ne_single_iff`, `ofFn_blocksFun`, `one_le_blocks`, `one_le_blocks'`, `one_le_blocksFun`, `ones_blocks`, `ones_blocksFun`, `ones_embedding`, `ones_length`, `ones_sizeUpTo`, `orderEmbOfFin_boundaries`, `reverse_append`, `reverse_bijective`, `reverse_blocks`, `reverse_eq_ones`, `reverse_eq_single`, `reverse_inj`, `reverse_injective`, `reverse_involutive`, `reverse_ones`, `reverse_reverse`, `reverse_single`, `reverse_surjective`, `sigma_eq_iff_blocks_eq`, `single_blocks`, `single_blocksFun`, `single_embedding`, `single_length`, `sizeUpTo_index_le`, `sizeUpTo_le`, `sizeUpTo_length`, `sizeUpTo_ofLength_le`, `sizeUpTo_strict_mono`, `sizeUpTo_succ`, `sizeUpTo_succ'`, `sizeUpTo_zero`, `sum_blocksFun`, `toCompositionAsSet_blocks`, `toCompositionAsSet_boundaries`, `toCompositionAsSet_length`, `blocksFun_pos`, `blocks_length`, `blocks_partial_sum`, `blocks_sum`, `boundaries_nonempty`, `boundary_length`, `boundary_zero`, `card_boundaries_eq_succ_length`, `card_boundaries_pos`, `ext`, `ext_iff`, `getLast_mem`, `length_lt_card_boundaries`, `lt_length`, `lt_length'`, `mem_boundaries_iff_exists_blocks_sum_take_eq`, `toComposition_blocks`, `toComposition_boundaries`, `toComposition_length`, `zero_mem`, `flatten_splitWrtComposition`, `flatten_splitWrtCompositionAux`, `getElem_splitWrtComposition`, `getElem_splitWrtComposition'`, `getElem_splitWrtCompositionAux`, `length_pos_of_mem_splitWrtComposition`, `length_splitWrtComposition`, `length_splitWrtCompositionAux`, `map_length_splitWrtComposition`, `map_length_splitWrtCompositionAux`, `splitWrtCompositionAux_cons`, `splitWrtComposition_flatten`, `sum_take_map_length_splitWrtComposition`, `compositionAsSet_card`, `composition_card`	115
Total	153

Composition

Definitions

Name	Category	Theorems
`append` 📖	CompOp	2 math math: `append_blocks`, `reverse_append`
`blocks` 📖	CompOp	22 math math: `ofFn_blocksFun`, `append_blocks`, `ext_iff`, `blocks_pos'`, `cast_blocks`, `Nat.Partition.ofComposition_parts`, `one_le_blocks'`, `blocksFun_mem_blocks`, `blocks_sum`, `ne_ones_iff`, `sigma_pi_composition_eq_iff`, `toCompositionAsSet_blocks`, `sizeUpTo_succ`, `List.map_length_splitWrtComposition`, `CompositionAsSet.toComposition_blocks`, `blocks_eq_nil`, `sigma_eq_iff_blocks_eq`, `sigma_composition_eq_iff`, `ones_blocks`, `blocks_length`, `reverse_blocks`, `single_blocks`
`blocksFinEquiv` 📖	CompOp	—
`blocksFun` 📖	CompOp	30 math math: `ofFn_blocksFun`, `embedding_comp_inv`, `blocksFun_sigmaCompositionAux`, `sum_blocksFun`, `length_sigmaCompositionAux`, `ones_blocksFun`, `FormalMultilinearSeries.compAlongComposition_nnnorm`, `blocksFun_le`, `index_embedding`, `FormalMultilinearSeries.compAlongComposition_bound`, `FormalMultilinearSeries.compChangeOfVariables_blocksFun`, `blocksFun_mem_blocks`, `sizeUpTo_succ'`, `FormalMultilinearSeries.compAlongComposition_norm`, `blocksFun_congr`, `mem_range_embedding`, `invEmbedding_comp`, `mem_range_embedding_iff'`, `sigma_pi_composition_eq_iff`, `FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1`, `disjoint_range`, `ne_single_iff`, `FormalMultilinearSeries.applyComposition_update`, `coe_invEmbedding`, `single_blocksFun`, `coe_embedding`, `FormalMultilinearSeries.mem_compPartialSumTarget_iff`, `mem_range_embedding_iff`, `single_embedding`, `one_le_blocksFun`
`boundaries` 📖	CompOp	4 math math: `orderEmbOfFin_boundaries`, `card_boundaries_eq_succ_length`, `CompositionAsSet.toComposition_boundaries`, `toCompositionAsSet_boundaries`
`boundary` 📖	CompOp	3 math math: `orderEmbOfFin_boundaries`, `boundary_zero`, `boundary_last`
`cast` 📖	CompOp	5 math math: `cast_blocks`, `cast_rfl`, `cast_heq`, `reverse_append`, `cast_eq_cast`
`embedding` 📖	CompOp	12 math math: `embedding_comp_inv`, `blocksFun_sigmaCompositionAux`, `index_embedding`, `mem_range_embedding`, `invEmbedding_comp`, `mem_range_embedding_iff'`, `ones_embedding`, `disjoint_range`, `FormalMultilinearSeries.applyComposition_update`, `coe_embedding`, `mem_range_embedding_iff`, `single_embedding`
`index` 📖	CompOp	9 math math: `embedding_comp_inv`, `index_embedding`, `sizeUpTo_index_le`, `mem_range_embedding`, `invEmbedding_comp`, `mem_range_embedding_iff'`, `lt_sizeUpTo_index_succ`, `FormalMultilinearSeries.applyComposition_update`, `coe_invEmbedding`
`instInhabited` 📖	CompOp	—
`instToString` 📖	CompOp	—
`invEmbedding` 📖	CompOp	4 math math: `embedding_comp_inv`, `invEmbedding_comp`, `FormalMultilinearSeries.applyComposition_update`, `coe_invEmbedding`
`length` 📖	CompOp	47 math math: `orderEmbOfFin_boundaries`, `FormalMultilinearSeries.comp_rightInv_aux1`, `ofFn_blocksFun`, `index_exists`, `List.length_splitWrtComposition`, `blocksFun_sigmaCompositionAux`, `sum_blocksFun`, `length_sigmaCompositionAux`, `length_pos_iff`, `card_boundaries_eq_succ_length`, `FormalMultilinearSeries.compAlongComposition_nnnorm`, `ones_length`, `CompositionAsSet.toComposition_length`, `FormalMultilinearSeries.compAlongComposition_bound`, `single_length`, `length_gather`, `FormalMultilinearSeries.compChangeOfVariables_blocksFun`, `boundary_zero`, `FormalMultilinearSeries.compChangeOfVariables_length`, `length_eq_zero`, `eq_ones_iff_length`, `sizeUpTo_succ'`, `eq_ones_iff_le_length`, `FormalMultilinearSeries.compAlongComposition_norm`, `sizeUpTo_index_le`, `length_pos_of_pos`, `length_le`, `sigma_pi_composition_eq_iff`, `ones_embedding`, `FormalMultilinearSeries.compAlongComposition_apply`, `FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1`, `toCompositionAsSet_length`, `ContinuousMultilinearMap.compAlongComposition_apply`, `lt_sizeUpTo_index_succ`, `boundary_last`, `sigma_composition_eq_iff`, `eq_single_iff_length`, `FormalMultilinearSeries.applyComposition_update`, `coe_invEmbedding`, `FormalMultilinearSeries.rightInv_coeff`, `FormalMultilinearSeries.comp_rightInv_aux2`, `sizeUpTo_length`, `coe_embedding`, `FormalMultilinearSeries.mem_compPartialSumTarget_iff`, `blocks_length`, `mem_range_embedding_iff`, `FormalMultilinearSeries.applyComposition_ones`
`ones` 📖	CompOp	10 math math: `ones_blocksFun`, `ones_length`, `eq_ones_iff`, `eq_ones_iff_length`, `ones_sizeUpTo`, `eq_ones_iff_le_length`, `ones_blocks`, `reverse_eq_ones`, `reverse_ones`, `FormalMultilinearSeries.applyComposition_ones`
`recOnAppendSingle` 📖	CompOp	—
`recOnSingleAppend` 📖	CompOp	—
`reverse` 📖	CompOp	12 math math: `reverse_bijective`, `reverse_eq_single`, `reverse_surjective`, `reverse_involutive`, `reverse_inj`, `reverse_injective`, `reverse_reverse`, `reverse_append`, `reverse_eq_ones`, `reverse_ones`, `reverse_blocks`, `reverse_single`
`single` 📖	CompOp	8 math math: `reverse_eq_single`, `single_length`, `FormalMultilinearSeries.applyComposition_single`, `eq_single_iff_length`, `single_blocksFun`, `reverse_single`, `single_blocks`, `single_embedding`
`sizeUpTo` 📖	CompOp	19 math math: `index_exists`, `sizeUpTo_le`, `List.sum_take_map_length_splitWrtComposition`, `ones_sizeUpTo`, `sizeUpTo_succ'`, `sizeUpTo_index_le`, `sizeUpTo_sizeUpTo_add`, `sizeUpTo_strict_mono`, `sizeUpTo_succ`, `monotone_sizeUpTo`, `List.getElem_splitWrtComposition'`, `lt_sizeUpTo_index_succ`, `sizeUpTo_ofLength_le`, `coe_invEmbedding`, `sizeUpTo_zero`, `sizeUpTo_length`, `coe_embedding`, `mem_range_embedding_iff`, `List.getElem_splitWrtComposition`
`toCompositionAsSet` 📖	CompOp	3 math math: `toCompositionAsSet_blocks`, `toCompositionAsSet_length`, `toCompositionAsSet_boundaries`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_blocks` 📖	mathematical	—	`blocks` `append`	—	—
`blocksFun_congr` 📖	mathematical	`blocks` `length`	`blocksFun`	—	`ext_iff`
`blocksFun_le` 📖	mathematical	—	`blocksFun`	—	`blocks_le`
`blocksFun_mem_blocks` 📖	mathematical	—	`blocks` `blocksFun`	—	—
`blocks_eq_nil` 📖	mathematical	—	`blocks`	—	`blocks_sum` `nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `length_le`
`blocks_le` 📖	—	`blocks`	—	—	`blocks_sum` `List.le_sum_of_mem` `Nat.instCanonicallyOrderedAdd`
`blocks_length` 📖	mathematical	—	`blocks` `length`	—	—
`blocks_pos` 📖	—	`blocks`	—	—	—
`blocks_pos'` 📖	mathematical	`length`	`blocks`	—	`one_le_blocks'`
`blocks_sum` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `blocks`	—	—
`boundary_last` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `length` `instFunLikeOrderEmbedding` `boundary`	—	`sizeUpTo_length`
`boundary_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `length` `instFunLikeOrderEmbedding` `boundary`	—	`sizeUpTo_zero`
`card_boundaries_eq_succ_length` 📖	mathematical	—	`Finset.card` `boundaries` `length`	—	`Finset.card_map` `Fintype.card_fin`
`cast_blocks` 📖	mathematical	—	`blocks` `cast`	—	—
`cast_eq_cast` 📖	mathematical	—	`cast` `Composition`	—	—
`cast_heq` 📖	mathematical	—	`Composition` `cast`	—	—
`cast_rfl` 📖	mathematical	—	`cast`	—	—
`coe_embedding` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `blocksFun` `instFunLikeOrderEmbedding` `embedding` `sizeUpTo` `length`	—	—
`coe_invEmbedding` 📖	mathematical	—	`blocksFun` `index` `invEmbedding` `sizeUpTo` `length`	—	—
`disjoint_range` 📖	mathematical	—	`Disjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.range` `blocksFun` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding`	—	`Set.not_disjoint_iff` `lt_irrefl` `mem_range_embedding_iff` `List.monotone_sum_take` `Nat.instCanonicallyOrderedAdd` `Disjoint.symm` `Ne.lt_or_gt`
`embedding_comp_inv` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `blocksFun` `index` `instFunLikeOrderEmbedding` `embedding` `invEmbedding`	—	`add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `sizeUpTo_index_le`
`eq_ones_iff` 📖	mathematical	—	`ones`	—	`ext` `blocks_sum` `List.sum_replicate` `mul_one` `ones_blocks`
`eq_ones_iff_le_length` 📖	mathematical	—	`ones` `length`	—	`length_le`
`eq_ones_iff_length` 📖	mathematical	—	`ones` `length`	—	`ones_length` `Mathlib.Tactic.Contrapose.contrapose₁` `lt_irrefl` `Finset.sum_const` `Fintype.card_congr'` `Fintype.card_fin` `mul_one` `ne_ones_iff` `Set.mem_range` `List.mem_ofFn'` `ofFn_blocksFun` `Finset.sum_lt_sum` `Nat.instIsOrderedCancelAddMonoid` `one_le_blocksFun` `Finset.mem_univ` `sum_blocksFun`
`eq_single_iff_length` 📖	mathematical	—	`single` `length`	—	`single_length` `ext` `blocks_length` `blocks_sum` `List.eq_cons_of_length_one` `add_zero`
`ext` 📖	—	`blocks`	—	—	—
`ext_iff` 📖	mathematical	—	`blocks`	—	`ext`
`index_embedding` 📖	mathematical	—	`index` `DFunLike.coe` `OrderEmbedding` `blocksFun` `instFunLikeOrderEmbedding` `embedding`	—	`mem_range_embedding_iff'` `Set.mem_range_self`
`index_exists` 📖	mathematical	—	`sizeUpTo` `length`	—	`lt_of_le_of_lt` `zero_le` `Nat.instCanonicallyOrderedAdd` `blocks_sum` `List.length_pos_of_sum_pos` `sizeUpTo_length` `ne_of_gt`
`invEmbedding_comp` 📖	mathematical	—	`blocksFun` `index` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding` `invEmbedding`	—	`index_embedding` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`length_eq_zero` 📖	mathematical	—	`length`	—	—
`length_le` 📖	mathematical	—	`length`	—	`blocks_sum` `List.length_le_sum_of_one_le` `one_le_blocks`
`length_pos_iff` 📖	mathematical	—	`length`	—	`Nat.instCanonicallyOrderedAdd`
`length_pos_of_pos` 📖	mathematical	—	`length`	—	`length_pos_iff`
`lt_sizeUpTo_index_succ` 📖	mathematical	—	`sizeUpTo` `length` `index`	—	`index_exists` `Nat.find_spec`
`mem_range_embedding` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `blocksFun` `index` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding`	—	`Set.mem_range_self` `embedding_comp_inv`
`mem_range_embedding_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `blocksFun` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding` `sizeUpTo` `length`	—	`Set.mem_range` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `sizeUpTo_succ'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `tsub_lt_iff_left` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instOrderedSub` `add_tsub_cancel_of_le`
`mem_range_embedding_iff'` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `blocksFun` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding` `index`	—	`not_imp_not` `Set.disjoint_right` `disjoint_range` `mem_range_embedding`
`monotone_sizeUpTo` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `sizeUpTo`	—	`List.monotone_sum_take` `Nat.instCanonicallyOrderedAdd`
`ne_ones_iff` 📖	mathematical	—	`blocks`	—	`eq_ones_iff` `one_le_blocks`
`ne_single_iff` 📖	mathematical	—	`blocksFun`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₂` `Mathlib.Tactic.Push.not_forall_eq` `single_blocksFun` `eq_single_iff_length` `lt_irrefl` `sum_blocksFun` `Finset.single_lt_sum` `Nat.instIsOrderedCancelAddMonoid` `Finset.mem_univ` `one_le_blocksFun` `zero_le` `Nat.instCanonicallyOrderedAdd` `Fintype.card_fin` `Fintype.card_eq_one_of_forall_eq`
`ofFn_blocksFun` 📖	mathematical	—	`length` `blocksFun` `blocks`	—	`List.ofFn_get`
`one_le_blocks` 📖	—	`blocks`	—	—	`blocks_pos`
`one_le_blocks'` 📖	mathematical	`length`	`blocks`	—	`one_le_blocks`
`one_le_blocksFun` 📖	mathematical	—	`blocksFun`	—	`one_le_blocks` `blocksFun_mem_blocks`
`ones_blocks` 📖	mathematical	—	`blocks` `ones`	—	—
`ones_blocksFun` 📖	mathematical	—	`blocksFun` `ones`	—	—
`ones_embedding` 📖	mathematical	`blocksFun` `ones`	`DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `embedding` `length` `lt_of_lt_of_le` `Nat.instPreorder` `length_le`	—	`lt_of_lt_of_le` `length_le` `ones_sizeUpTo` `add_zero` `ones_length` `LT.lt.le`
`ones_length` 📖	mathematical	—	`length` `ones`	—	—
`ones_sizeUpTo` 📖	mathematical	—	`sizeUpTo` `ones`	—	`List.sum_replicate` `mul_one`
`orderEmbOfFin_boundaries` 📖	mathematical	—	`Finset.orderEmbOfFin` `Fin.instLinearOrder` `boundaries` `length` `card_boundaries_eq_succ_length` `boundary`	—	`card_boundaries_eq_succ_length` `Finset.orderEmbOfFin_unique'` `Finset.mem_map'` `Finset.mem_univ`
`reverse_append` 📖	mathematical	—	`reverse` `append` `cast` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Nat.instAddCommSemigroup` `add_comm`	—	`ext` `add_comm`
`reverse_bijective` 📖	mathematical	—	`Function.Bijective` `Composition` `reverse`	—	`Function.Involutive.bijective` `reverse_involutive`
`reverse_blocks` 📖	mathematical	—	`blocks` `reverse`	—	—
`reverse_eq_ones` 📖	mathematical	—	`reverse` `ones`	—	`reverse_injective` `reverse_ones`
`reverse_eq_single` 📖	mathematical	—	`reverse` `single`	—	`reverse_injective` `reverse_single`
`reverse_inj` 📖	mathematical	—	`reverse`	—	`reverse_injective`
`reverse_injective` 📖	mathematical	—	`Composition` `reverse`	—	`Function.Involutive.injective` `reverse_involutive`
`reverse_involutive` 📖	mathematical	—	`Function.Involutive` `Composition` `reverse`	—	`reverse_reverse`
`reverse_ones` 📖	mathematical	—	`reverse` `ones`	—	`ext`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	`ext`
`reverse_single` 📖	mathematical	—	`reverse` `single`	—	`ext`
`reverse_surjective` 📖	mathematical	—	`Composition` `reverse`	—	`Function.Involutive.surjective` `reverse_involutive`
`sigma_eq_iff_blocks_eq` 📖	mathematical	—	`blocks` `Composition`	—	`blocks_sum` `ext`
`single_blocks` 📖	mathematical	—	`blocks` `single`	—	—
`single_blocksFun` 📖	mathematical	—	`blocksFun` `single`	—	—
`single_embedding` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `blocksFun` `single` `instFunLikeOrderEmbedding` `embedding`	—	`sizeUpTo_zero` `zero_add`
`single_length` 📖	mathematical	—	`length` `single`	—	—
`sizeUpTo_index_le` 📖	mathematical	—	`sizeUpTo` `length` `index`	—	`nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `sizeUpTo_zero` `ne_of_gt` `Nat.find_min` `index_exists` `lt_trans`
`sizeUpTo_le` 📖	mathematical	—	`sizeUpTo`	—	`blocks_sum` `List.sum_take_add_sum_drop`
`sizeUpTo_length` 📖	mathematical	—	`sizeUpTo` `length`	—	`sizeUpTo_ofLength_le` `le_rfl`
`sizeUpTo_ofLength_le` 📖	mathematical	`length`	`sizeUpTo`	—	`blocks_sum`
`sizeUpTo_strict_mono` 📖	mathematical	`length`	`sizeUpTo`	—	`sizeUpTo_succ` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le`
`sizeUpTo_succ` 📖	mathematical	`length`	`sizeUpTo` `blocks`	—	`List.sum_take_succ`
`sizeUpTo_succ'` 📖	mathematical	—	`sizeUpTo` `length` `blocksFun`	—	`sizeUpTo_succ`
`sizeUpTo_zero` 📖	mathematical	—	`sizeUpTo`	—	—
`sum_blocksFun` 📖	mathematical	—	`Finset.sum` `length` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype` `blocksFun`	—	`blocks_sum` `ofFn_blocksFun` `List.sum_ofFn`
`toCompositionAsSet_blocks` 📖	mathematical	—	`CompositionAsSet.blocks` `toCompositionAsSet` `blocks`	—	`CompositionAsSet.blocks_length` `toCompositionAsSet_length` `CompositionAsSet.card_boundaries_eq_succ_length` `card_boundaries_eq_succ_length` `CompositionAsSet.blocks_partial_sum` `CompositionAsSet.boundary.eq_1` `sizeUpTo.eq_1` `orderEmbOfFin_boundaries` `List.eq_of_sum_take_eq`
`toCompositionAsSet_boundaries` 📖	mathematical	—	`CompositionAsSet.boundaries` `toCompositionAsSet` `boundaries`	—	—
`toCompositionAsSet_length` 📖	mathematical	—	`CompositionAsSet.length` `toCompositionAsSet` `length`	—	`card_boundaries_eq_succ_length` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`

CompositionAsSet

Definitions

Name	Category	Theorems
`blocks` 📖	CompOp	6 math math: `blocks_partial_sum`, `Composition.toCompositionAsSet_blocks`, `blocks_sum`, `toComposition_blocks`, `mem_boundaries_iff_exists_blocks_sum_take_eq`, `blocks_length`
`blocksFun` 📖	CompOp	1 math math: `blocksFun_pos`
`boundaries` 📖	CompOp	14 math math: `card_boundaries_eq_succ_length`, `card_boundaries_pos`, `boundaries_nonempty`, `length_lt_card_boundaries`, `ext_iff`, `getLast_mem`, `lt_length'`, `zero_mem`, `lt_length`, `toComposition_boundaries`, `mem_boundaries_iff_exists_blocks_sum_take_eq`, `Composition.toCompositionAsSet_boundaries`, `boundary_length`, `boundary_zero`
`boundary` 📖	CompOp	3 math math: `blocks_partial_sum`, `boundary_length`, `boundary_zero`
`length` 📖	CompOp	8 math math: `card_boundaries_eq_succ_length`, `length_lt_card_boundaries`, `toComposition_length`, `lt_length'`, `lt_length`, `Composition.toCompositionAsSet_length`, `boundary_length`, `blocks_length`
`toComposition` 📖	CompOp	3 math math: `toComposition_length`, `toComposition_blocks`, `toComposition_boundaries`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`blocksFun_pos` 📖	mathematical	—	`blocksFun`	—	`lt_length` `lt_length'` `lt_tsub_iff_left` `Nat.instOrderedSub` `OrderEmbedding.strictMono`
`blocks_length` 📖	mathematical	—	`blocks` `length`	—	—
`blocks_partial_sum` 📖	mathematical	`Finset.card` `boundaries`	`MulZeroClass.toZero` `Nat.instMulZeroClass` `blocks` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `boundary`	—	`boundary_zero` `card_boundaries_eq_succ_length` `lt_of_lt_of_le` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `List.sum_take_succ` `lt_length` `lt_length'` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE`
`blocks_sum` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `blocks`	—	`length_lt_card_boundaries` `blocks_partial_sum` `boundary_length`
`boundaries_nonempty` 📖	mathematical	—	`Finset.Nonempty` `boundaries`	—	`zero_mem`
`boundary_length` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Finset.card` `boundaries` `instFunLikeOrderEmbedding` `boundary` `length` `length_lt_card_boundaries`	—	`length_lt_card_boundaries` `card_boundaries_pos` `Finset.card_pos` `le_antisymm` `Finset.le_max'` `getLast_mem` `Finset.orderEmbOfFin_last`
`boundary_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Finset.card` `boundaries` `instFunLikeOrderEmbedding` `boundary` `card_boundaries_pos`	—	`card_boundaries_pos` `boundary.eq_1` `Finset.card_pos` `Finset.orderEmbOfFin_zero` `le_antisymm` `Finset.min'_le` `zero_mem`
`card_boundaries_eq_succ_length` 📖	mathematical	—	`Finset.card` `boundaries` `length`	—	`tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `card_boundaries_pos`
`card_boundaries_pos` 📖	mathematical	—	`Finset.card` `boundaries`	—	`Finset.card_pos` `boundaries_nonempty`
`ext` 📖	—	`boundaries`	—	—	—
`ext_iff` 📖	mathematical	—	`boundaries`	—	`ext`
`getLast_mem` 📖	mathematical	—	`Finset` `Finset.instMembership` `boundaries`	—	—
`length_lt_card_boundaries` 📖	mathematical	—	`length` `Finset.card` `boundaries`	—	`card_boundaries_eq_succ_length`
`lt_length` 📖	mathematical	—	`length` `Finset.card` `boundaries`	—	`lt_tsub_iff_right` `Nat.instOrderedSub`
`lt_length'` 📖	mathematical	—	`length` `Finset.card` `boundaries`	—	`lt_of_le_of_lt` `lt_length`
`mem_boundaries_iff_exists_blocks_sum_take_eq` 📖	mathematical	—	`Finset` `Finset.instMembership` `boundaries` `Finset.card` `MulZeroClass.toZero` `Nat.instMulZeroClass` `blocks`	—	`OrderIso.surjective` `blocks_partial_sum`
`toComposition_blocks` 📖	mathematical	—	`Composition.blocks` `toComposition` `blocks`	—	—
`toComposition_boundaries` 📖	mathematical	—	`Composition.boundaries` `toComposition` `boundaries`	—	`Finset.ext` `toComposition_length` `mem_boundaries_iff_exists_blocks_sum_take_eq` `card_boundaries_eq_succ_length`
`toComposition_length` 📖	mathematical	—	`Composition.length` `toComposition` `length`	—	`blocks_length`
`zero_mem` 📖	mathematical	—	`Finset` `Finset.instMembership` `boundaries`	—	—

List

Definitions

Name	Category	Theorems
`splitWrtComposition` 📖	CompOp	5 math math: `length_splitWrtComposition`, `sum_take_map_length_splitWrtComposition`, `splitWrtComposition_flatten`, `map_length_splitWrtComposition`, `flatten_splitWrtComposition`
`splitWrtCompositionAux` 📖	CompOp	4 math math: `length_splitWrtCompositionAux`, `flatten_splitWrtCompositionAux`, `splitWrtCompositionAux_cons`, `map_length_splitWrtCompositionAux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flatten_splitWrtComposition` 📖	mathematical	—	`splitWrtComposition`	—	`flatten_splitWrtCompositionAux` `Composition.blocks_sum`
`flatten_splitWrtCompositionAux` 📖	mathematical	`MulZeroClass.toZero` `Nat.instMulZeroClass`	`splitWrtCompositionAux`	—	`splitWrtCompositionAux_cons` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`getElem_splitWrtComposition` 📖	mathematical	`splitWrtComposition`	`Composition.sizeUpTo`	—	`getElem_splitWrtComposition'`
`getElem_splitWrtComposition'` 📖	mathematical	`splitWrtComposition`	`Composition.sizeUpTo`	—	`getElem_splitWrtCompositionAux`
`getElem_splitWrtCompositionAux` 📖	mathematical	`splitWrtCompositionAux`	`MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`splitWrtCompositionAux_cons` `zero_add` `add_zero`
`length_pos_of_mem_splitWrtComposition` 📖	—	`splitWrtComposition`	—	—	`Composition.blocks_pos` `map_length_splitWrtComposition`
`length_splitWrtComposition` 📖	mathematical	—	`splitWrtComposition` `Composition.length`	—	`length_splitWrtCompositionAux`
`length_splitWrtCompositionAux` 📖	mathematical	—	`splitWrtCompositionAux`	—	`splitWrtCompositionAux_cons`
`map_length_splitWrtComposition` 📖	mathematical	—	`splitWrtComposition` `Composition.blocks`	—	`map_length_splitWrtCompositionAux` `le_of_eq` `Composition.blocks_sum`
`map_length_splitWrtCompositionAux` 📖	mathematical	`MulZeroClass.toZero` `Nat.instMulZeroClass`	`splitWrtCompositionAux`	—	`Nat.instCanonicallyOrderedAdd`
`splitWrtCompositionAux_cons` 📖	mathematical	—	`splitWrtCompositionAux`	—	—
`splitWrtComposition_flatten` 📖	mathematical	`Composition.blocks`	`splitWrtComposition`	—	`flatten_splitWrtComposition` `map_length_splitWrtComposition`
`sum_take_map_length_splitWrtComposition` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `splitWrtComposition` `Composition.sizeUpTo`	—	`map_length_splitWrtComposition`

(root)

Definitions

Name	Category	Theorems
`CompositionAsSet` 📖	CompData	1 math math: `compositionAsSet_card`
`compositionAsSetEquiv` 📖	CompOp	—
`compositionAsSetFintype` 📖	CompOp	1 math math: `compositionAsSet_card`
`compositionEquiv` 📖	CompOp	—
`compositionFintype` 📖	CompOp	5 math math: `FormalMultilinearSeries.comp_rightInv_aux1`, `composition_card`, `FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1`, `FormalMultilinearSeries.rightInv_coeff`, `FormalMultilinearSeries.comp_rightInv_aux2`
`instDecidableEqComposition` 📖	CompOp	—
`instDecidableEqCompositionAsSet` 📖	CompOp	—
`instInhabitedCompositionAsSet` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compositionAsSet_card` 📖	mathematical	—	`Fintype.card` `CompositionAsSet` `compositionAsSetFintype` `Monoid.toNatPow` `Nat.instMonoid`	—	`Fintype.card_finset` `Fintype.card_fin` `Fintype.card_congr`
`composition_card` 📖	mathematical	—	`Fintype.card` `Composition` `compositionFintype` `Monoid.toNatPow` `Nat.instMonoid`	—	`compositionAsSet_card` `Fintype.card_congr`

instDecidableEqComposition

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

instDecidableEqCompositionAsSet

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index