CompositionAsSet.getLast_mem
theorem CompositionAsSet.getLast_mem : ∀ {n : ℕ} (self : CompositionAsSet n), Fin.last n ∈ self.boundaries
The theorem `CompositionAsSet.getLast_mem` states that for any natural number `n` and any set composition of `n`, the greatest value of `Fin (n+1)` is always an element of the boundaries of the composition. In other words, if we have a composition of a natural number, the last element, represented by `Fin.last n`, is guaranteed to be within the boundary of this composition.
More concisely: For any natural number `n` and set composition `p` of `n+1`, `Fin.last n` is in the boundary of `p`.
|
Composition.disjoint_range
theorem Composition.disjoint_range :
∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
i₁ ≠ i₂ → Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
The theorem `Composition.disjoint_range` states that for any natural number `n` and any composition `c` of `n`, the embeddings of different blocks of this composition are disjoint. Here, "different blocks" are represented by two different elements `i₁` and `i₂` of the `Fin c.length`, where `i₁` is not equal to `i₂`. This disjointness is defined according to the `Disjoint` function, which in this context means that the intersection (infimum) of the ranges of the two embeddings is the empty set. In other words, no element in the range of `c.embedding i₁` is also in the range of `c.embedding i₂`, and vice versa.
More concisely: For any natural number `n` and composition `c` of `n`, the embeddings of different blocks of `c` have disjoint ranges, i.e., their intersection is the empty set.
|
Composition.sum_blocksFun
theorem Composition.sum_blocksFun : ∀ {n : ℕ} (c : Composition n), (Finset.univ.sum fun i => c.blocksFun i) = n := by
sorry
The theorem `Composition.sum_blocksFun` states that for any natural number `n` and any composition `c` of `n`, the sum of the values of the `blocksFun` function applied to each element in the universal finite set is equal to `n`. In other words, if you take a composition of a number, transform each block of the composition using the `blocksFun` function, and add up all the results, you'll get the original number back.
More concisely: For any natural number `n` and composition `c` of `n`, the sum of applying the function `blocksFun` to each block in `c` equals `n`.
|
Composition.index_exists
theorem Composition.index_exists :
∀ {n : ℕ} (c : Composition n) {j : ℕ}, j < n → ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length
The theorem `index_exists` establishes that for any natural number `n`, any composition `c` of `n`, and any natural number `j` that is less than `n`, there exists an index `i` such that `j` is less than the sum of the sizes of the blocks in the composition up to `i+1`, and `i` is less than the number of blocks in the composition. In other words, this theorem states that for any particular `j` within the range of the composition, we can always find a segment of the composition (up to a certain block `i+1`) where the total size of the blocks is greater than `j`, and that this `i` is within the length of the composition.
More concisely: For any composition `c` of a natural number `n` and any `0 < j < n`, there exists an index `i < n` such that the sum of the sizes of the first `i+1` blocks in `c` is greater than `j`.
|
CompositionAsSet.zero_mem
theorem CompositionAsSet.zero_mem : ∀ {n : ℕ} (self : CompositionAsSet n), 0 ∈ self.boundaries
This theorem states that `0` is a member of `boundaries` for any `CompositionAsSet` of a natural number `n`. Specifically, for every natural number `n`, and any instance `self` of the `CompositionAsSet` of `n`, `0` is always an element of the `boundaries` of `self`.
More concisely: For every natural number `n` and `CompositionAsSet` `self` of `n`, `0` is an element of `boundaries self`.
|
Composition.sizeUpTo_succ
theorem Composition.sizeUpTo_succ :
∀ {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length), c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks.get ⟨i, h⟩
The theorem `Composition.sizeUpTo_succ` states that for any natural number `n` and any composition `c` of `n`, and for any natural number `i` which is less than the length of the composition `c`, the sum of the sizes of the blocks in the composition up to `i + 1` is equal to the sum of the sizes of the blocks up to `i` plus the size of the block at position `i`. In other words, if you add another block to the sum, the total sum increases by the size of the new block.
More concisely: For any natural number `n` and composition `c` of `n`, and any `i` less than `c.size`, the sum of the sizes of the first `i+1` blocks in `c` equals the sum of the sizes of the first `i` blocks plus the size of the `i+1`th block.
|
Composition.sizeUpTo_length
theorem Composition.sizeUpTo_length : ∀ {n : ℕ} (c : Composition n), c.sizeUpTo c.length = n
This theorem states that for any natural number `n` and a composition `c` of `n`, the sum of the sizes of the blocks in the composition up to the length of the composition (i.e., the number of blocks in the composition) is equal to `n`. In other words, if you sum the sizes of all the blocks in a composition, you get the number that the composition is of. This is a fundamental property of compositions in combinatorics.
More concisely: For any natural number `n` and its composition `c`, the sum of the sizes of the blocks in `c` equals `n`.
|
Composition.ext
theorem Composition.ext : ∀ {n : ℕ} (x y : Composition n), x.blocks = y.blocks → x = y
This theorem, named `Composition.ext`, states that for any natural number `n`, given two compositions `x` and `y` of `n`, if the `blocks` of `x` and `y` are equal, then `x` and `y` are equal. In other words, the equality of two compositions is determined solely by the equality of their respective `blocks`.
More concisely: If two compositions of a natural number have equal blocks, then they are equal.
|
Composition.one_le_blocksFun
theorem Composition.one_le_blocksFun : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length), 1 ≤ c.blocksFun i
This theorem states that for any natural number `n` and any composition `c` of that number, the value of the `blocksFun` function at any index `i` (which is a finite number with bound `length c`) will always be greater than or equal to 1. In other words, every block in the composition has at least one element.
More concisely: For any natural number `n` and composition `c` of length `l` over `n`, the function `blocksFun` at index `i` (where `0 ≤ i < l`) satisfies `blocksFun i ≥ 1`.
|
Composition.boundary.proof_1
theorem Composition.boundary.proof_1 : ∀ {n : ℕ} (c : Composition n) (i : Fin (c.length + 1)), c.sizeUpTo ↑i < n.succ
This theorem states that for any natural number `n` and any composition `c` of `n`, if `i` is a natural number less than or equal to the length of the composition `c` plus one, then the sum of the sizes of the blocks in the composition `c` up to `i` is strictly less than `n+1`. In other words, the total size of the first `i` blocks in any composition of `n` is always less than `n+1`.
More concisely: For any natural number `n` and composition `c` of `n`, the sum of the sizes of the first `i` blocks in `c` is strictly less than `n + 1` for all `i` leq `length c + 1`.
|
List.get_splitWrtComposition'
theorem List.get_splitWrtComposition' :
∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) {i : ℕ} (hi : i < (l.splitWrtComposition c).length),
(l.splitWrtComposition c).get ⟨i, hi⟩ = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
This theorem states that for any given list `l` of elements of type `α` and a composition `c` of an integer `n`, the `i`-th sublist in the splitting of `l` along `c` equals to the slice of `l` between the indices `c.sizeUpTo i` and `c.sizeUpTo (i+1)`. Here, `i` is a natural number such that it is less than the length of the list resulted from splitting `l` with respect to `c`. This is equivalent to saying that the `i`-th sublist corresponds to the `i`-th block of the composition. The slice operation is defined as dropping the first `c.sizeUpTo i` elements from the list obtained by taking the first `c.sizeUpTo (i + 1)` elements from `l`.
More concisely: For any list `l` of length `m` and composition `c` of size `k`, the `i`-th sublist of `l` along `c` equals the slice of `l` from indices `c.sizeUpTo i` to `c.sizeUpTo (i+1)`, where `i` is a natural number less than `m/k`.
|
Composition.blocks_sum
theorem Composition.blocks_sum : ∀ {n : ℕ} (self : Composition n), self.blocks.sum = n
This theorem states that for any natural number `n` and any composition `self` of `n`, the sum of the elements (or blocks) in the composition is equal to `n`. In simpler terms, if you have a way to break down a number into smaller parts (a composition), and if you add up all those parts, you'll get the original number.
More concisely: For any natural number `n` and any composition `self` of `n`, the sum of the parts in `self` equals `n`.
|
List.splitWrtComposition_join
theorem List.splitWrtComposition_join :
∀ {α : Type u_1} (L : List (List α)) (c : Composition L.join.length),
List.map List.length L = c.blocks → L.join.splitWrtComposition c = L
This theorem states that for any type `α` and any list of lists `L` of type `α`, and any composition `c` of the length of the joined list `L`, if the list obtained by mapping each sublist of `L` to its length equals the blocks of `c`, then splitting the joined list `L` with respect to the composition `c` gives back the original list of lists `L`. In simple terms, it says that if we join a list of lists into a single list and then split it according to the original sub-list lengths, we retrieve the original list of lists.
More concisely: If `L` is a list of lists of type `α` and `c` is a composition of the length of each sublist in `L`, then splitting the joined list `map (length) L` according to `c` yields `L` itself.
|
Composition.blocks_pos
theorem Composition.blocks_pos : ∀ {n : ℕ} (self : Composition n) {i : ℕ}, i ∈ self.blocks → 0 < i
This theorem states that for a given composition of a natural number `n` (represented by `self`), if `i` is an element of the `blocks` of the composition, then `i` is strictly greater than 0. In mathematical terms, this theorem asserts the positivity of each block in any composition of a natural number.
More concisely: For any natural number composition `self`, every block `i` in the composition satisfies `i > 0`.
|
List.splitWrtCompositionAux_cons
theorem List.splitWrtCompositionAux_cons :
∀ {α : Type u_1} (l : List α) (n : ℕ) (ns : List ℕ),
l.splitWrtCompositionAux (n :: ns) = List.take n l :: (List.drop n l).splitWrtCompositionAux ns
The theorem `List.splitWrtCompositionAux_cons` states that for all types `α`, lists of `α` (denoted as `l`), and lists of natural numbers `n` and `ns`, the operation `List.splitWrtCompositionAux` applied to the list `l` and the list of natural numbers `n :: ns` is equal to the list constructed by taking the first `n` elements from `l` and appending the result of `List.splitWrtCompositionAux` applied to the remainder of the list after dropping the first `n` elements and the list `ns`. In other words, it describes how the `List.splitWrtCompositionAux` function behaves when splitting a list into sublists: it takes a certain number of elements from the front of the list, then recursively does the same to the rest of the list.
More concisely: For all types `α`, lists `l` of `α`, and lists `n :: ns` of natural numbers, `List.splitWrtCompositionAux l (n :: ns) = take n l ++ List.splitWrtCompositionAux (drop n l) ns`.
|
List.join_splitWrtComposition
theorem List.join_splitWrtComposition :
∀ {α : Type u_1} (l : List α) (c : Composition l.length), (l.splitWrtComposition c).join = l
This theorem states that for any given list `l` of a certain type `α` and any composition `c` of the length of `list`, if you first split the list `l` according to the composition `c` and then join the resulting sublists, you will get back the original list `l`. In other words, splitting the list into sublists according to a certain pattern (`composition`), and then concatenating those sublists will not change the original list.
More concisely: For any list `l` of type `α` and composition `c` of length matching `l.length`, the list obtained by splitting `l` according to `c` and then joining the resulting sublists is equal to the original list `l`.
|
Composition.one_le_blocks
theorem Composition.one_le_blocks : ∀ {n : ℕ} (c : Composition n) {i : ℕ}, i ∈ c.blocks → 1 ≤ i
This theorem, `Composition.one_le_blocks`, states that for any natural number `n` and any composition `c` of `n`, if `i` is an element in the list of blocks of `c`, then `i` is greater than or equal to 1. In other words, each block in a composition of a natural number is at least 1.
More concisely: For any natural number `n` and composition `c` of `n`, every block `i` in `c` satisfies `i ≥ 1`.
|
Composition.orderEmbOfFin_boundaries
theorem Composition.orderEmbOfFin_boundaries :
∀ {n : ℕ} (c : Composition n), c.boundaries.orderEmbOfFin ⋯ = c.boundary
This theorem states that for any natural number `n` and any composition `c` of `n`, the canonical increasing bijection between the finite set `Fin (c.length + 1)` and the set `c.boundaries` is precisely the function `c.boundary`. A composition in this context is a way of writing `n` as a sum of positive integers, and `c.boundaries` represents the set of boundaries that divide up `n` according to the composition. The theorem is stating that the standard increasing bijection corresponds exactly to the boundary function of the composition.
More concisely: The function `c.boundary` is the canonical increasing bijection between the finite set with `length (c.length + 1)` and the set of boundaries of a composition `c` of a natural number `n`.
|
Composition.ofFn_blocksFun
theorem Composition.ofFn_blocksFun : ∀ {n : ℕ} (c : Composition n), List.ofFn c.blocksFun = c.blocks
This theorem, `Composition.ofFn_blocksFun`, states that for any natural number `n` and any composition `c` of `n`, the list created by applying the function `Composition.blocksFun c` to each index of the composition (from 0 to `Composition.length c - 1`) is equal to the list of blocks in the composition `c`. In other words, it asserts that the function `Composition.blocksFun` retrieves the blocks of the composition when applied to each element of the finite set `Fin (Composition.length c)`, and the resulting list of these blocks is exactly the same as the original list of blocks in the composition.
More concisely: For any composition `c` of length `n`, the list of blocks obtained by applying `Composition.blocksFun` to each index in `Fin n` equals the original list of blocks in `c`.
|
List.map_length_splitWrtComposition
theorem List.map_length_splitWrtComposition :
∀ {α : Type u_1} (l : List α) (c : Composition l.length),
List.map List.length (l.splitWrtComposition c) = c.blocks
This theorem states that for any given list `l` of type `α` and a composition `c` of the length of `l`, when the list `l` is split according to the composition `c` using the function `List.splitWrtComposition`, if we then take the lengths of the resulting sublists using `List.map List.length`, we obtain the original composition `c.blocks`. In essence, it shows that splitting a list based on a composition yields sublists whose lengths correspond to the block sizes in the composition.
More concisely: Given a list `l` of type `α` and a composition `c` of length `l.size`, the lengths of the sublists obtained by splitting `l` according to `c` using `List.splitWrtComposition` equal `c.blocks`.
|
Composition.sizeUpTo_zero
theorem Composition.sizeUpTo_zero : ∀ {n : ℕ} (c : Composition n), c.sizeUpTo 0 = 0
This theorem states that for any natural number `n` and any composition `c` of `n`, the size up to the zeroth block in the composition is zero. In other words, there are no blocks to sum in the composition prior to the first block, so the sum is zero. This is analogous to the mathematical statement that the sum of an empty set of numbers is zero.
More concisely: The size of the zeroth block in any composition is zero.
|
Composition.sigma_eq_iff_blocks_eq
theorem Composition.sigma_eq_iff_blocks_eq :
∀ {c c' : (n : ℕ) × Composition n}, c = c' ↔ c.snd.blocks = c'.snd.blocks
This theorem states that two compositions (`c` and `c'`), which may be of different natural numbers (`n`), are equal if and only if they have the same sequence of blocks. In other words, if two compositions have the same sequence of blocks, then they are the same composition, and conversely, if they are the same composition, then they must have the same sequence of blocks.
More concisely: Two compositions of natural numbers are equal if and only if they have the same sequence of blocks.
|
List.length_splitWrtComposition
theorem List.length_splitWrtComposition :
∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n), (l.splitWrtComposition c).length = c.length
The theorem `List.length_splitWrtComposition` states that if you split a list `l` according to a composition `c`, the total number of sublists created in this process is equal to the number of blocks in the composition `c`. In other words, the length of the list obtained by splitting list `l` with respect to composition `c` is equal to the length of the composition `c`.
More concisely: The length of a list split by a composition equals the number of blocks in the composition.
|