YoungDiagram.rowLens_length_ofRowLens
theorem YoungDiagram.rowLens_length_ofRowLens :
∀ {w : List ℕ} {hw : List.Sorted (fun x x_1 => x ≥ x_1) w},
(∀ x ∈ w, 0 < x) → (YoungDiagram.ofRowLens w hw).rowLens.length = w.length
This theorem states that the number of rows in a Young diagram constructed from a sorted list `w`, with a sorting rule stating that any element `x` in `w` is greater than or equal to any subsequent element `x_1`, is equal to the length of `w`. This is provided that all elements in `w` are positive numbers (greater than 0). In other words, the length of the rows in the Young diagram (represented as `.rowLens.length`) corresponds directly to the number of elements in the input list `w`.
More concisely: The length of a Young diagram constructed from a sorted and positive list equals the list's length.
|
YoungDiagram.rowLens_sorted
theorem YoungDiagram.rowLens_sorted : ∀ (μ : YoungDiagram), List.Sorted (fun x x_1 => x ≥ x_1) μ.rowLens
This theorem states that for any Young diagram `μ`, the list of its row lengths, obtained by the function `YoungDiagram.rowLens`, is sorted in a non-increasing order. In other words, for any two elements `x` and `x_1` in the list, `x` is greater than or equal to `x_1`. The relation `x ≥ x_1` is a "greater than or equal to" relation, which is transitive and antisymmetric.
More concisely: For any Young diagram, the list of its row lengths, as obtained by `YoungDiagram.rowLens`, is non-decreasing.
|
YoungDiagram.exists_not_mem_col
theorem YoungDiagram.exists_not_mem_col : ∀ (μ : YoungDiagram) (j : ℕ), ∃ i, (i, j) ∉ μ.cells
This theorem states that for any given Young Diagram `μ` and any natural number `j`, there exists a natural number `i` such that the cell `(i, j)` is not a member of the set of cells of `μ`. In other words, no matter what column `j` we choose, we can always find a row `i` where there isn't a cell at the position `(i, j)` in the Young Diagram `μ`.
More concisely: For any Young Diagram `μ` and natural number `j`, there exists a row index `i` such that `(i, j)` is not in `μ`.
|
YoungDiagram.ofRowLens_to_rowLens_eq_self
theorem YoungDiagram.ofRowLens_to_rowLens_eq_self : ∀ {μ : YoungDiagram}, YoungDiagram.ofRowLens μ.rowLens ⋯ = μ := by
sorry
This theorem states that for any Young diagram `μ`, when we convert the row lengths of `μ` into a Young diagram using the `YoungDiagram.ofRowLens` function and then convert it back to row lengths, we end up with the original Young diagram `μ`. In other words, the function `YoungDiagram.ofRowLens` is left invertible with respect to the operation of taking row lengths, thereby preserving the structure of the original Young diagram.
More concisely: The `YoungDiagram.ofRowLens` function is a left-inverse for taking row lengths in the context of Young diagrams.
|
YoungDiagram.up_left_mem
theorem YoungDiagram.up_left_mem :
∀ (μ : YoungDiagram) {i1 i2 j1 j2 : ℕ}, i1 ≤ i2 → j1 ≤ j2 → (i2, j2) ∈ μ → (i1, j1) ∈ μ
The theorem `YoungDiagram.up_left_mem` states that for any Young diagram `μ` and for any four natural numbers i1, i2, j1, j2, if i1 is less than or equal to i2 and j1 is less than or equal to j2, and if the pair (i2, j2) is in `μ`, then the pair (i1, j1) is also in `μ`. In other words, if a point is in the Young diagram, then any point weakly up-and-left of it is also in the diagram.
More concisely: If (i1, j1) is a weakly northwest lying cell of a Young diagram μ, and (i2, j2) is a cell in μ with i1 ≤ i2 and j1 ≤ j2, then (i1, j1) is also in μ.
|
Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.29
theorem Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.29 :
∀ {w : List ℕ} {hw : List.Sorted (fun x x_1 => x ≥ x_1) w} {c : ℕ × ℕ},
(c ∈ YoungDiagram.ofRowLens w hw) = ∃ (h : c.1 < w.length), c.2 < w.get ⟨c.1, h⟩
This theorem states that for any list `w` of natural numbers that is sorted in non-increasing order (`hw` is the proof of this property), and for any pair of natural numbers `c`, the pair `c` is in the YoungDiagram formed from the list `w` if and only if there exists a proof `h` such that the first element of `c`, `c.1`, is less than the length of the list `w` and the second element of `c`, `c.2`, is less than the element at index `c.1` in the list `w`.
More concisely: For a sorted list `w` of natural numbers and a pair `c`, `c` is in the Young Diagram formed from `w` if and only if `c.1 < length w` and `c.2 < w!(c.1)`.
|
YoungDiagram.exists_not_mem_row
theorem YoungDiagram.exists_not_mem_row : ∀ (μ : YoungDiagram) (i : ℕ), ∃ j, (i, j) ∉ μ
This theorem states that for every Young Diagram, represented by `μ`, and for any natural number `i`, there exists a natural number `j` such that the pair `(i, j)` does not belong to `μ`. In other words, it's saying that no matter what row `i` we are looking at in the Young Diagram, there is always a column `j` that is not in that row.
More concisely: For every Young Diagram `μ` and natural number `i`, there exists a natural number `j` such that `(i, j)` is not in `μ`.
|
YoungDiagram.rowLens_ofRowLens_eq_self
theorem YoungDiagram.rowLens_ofRowLens_eq_self :
∀ {w : List ℕ} {hw : List.Sorted (fun x x_1 => x ≥ x_1) w},
(∀ x ∈ w, 0 < x) → (YoungDiagram.ofRowLens w hw).rowLens = w
This theorem is asserting the "right inverse" direction of an equivalence relation. Specifically, it states that for any list of natural numbers, `w`, that is sorted in descending order (i.e., each number `x` in the list is greater than or equal to the next number `x_1`), if all numbers in `w` are positive (i.e., greater than zero), then the list of row lengths of the Young Diagram constructed from `w` is identical to `w` itself. The Young Diagram is constructed using the `YoungDiagram.ofRowLens` function, which turns a sorted list into a Young Diagram.
More concisely: If `w` is a sorted list of positive natural numbers, then the Young Diagram constructed from `w` using `YoungDiagram.ofRowLens` is identical to `w`.
|
YoungDiagram.isLowerSet
theorem YoungDiagram.isLowerSet : ∀ (self : YoungDiagram), IsLowerSet ↑self.cells
The theorem `YoungDiagram.isLowerSet` states that for any Young Diagram, the set of its cells is a lower set in the order of natural number pairs. In other words, if we have a cell (a, b) in the Young Diagram, then any cell (c, d) with c ≤ a and d ≤ b is also in the Young Diagram. This reflects the fact that the cells in a Young Diagram are "up-left justified".
More concisely: The Young Diagram's cell set is a lower set in the order of natural number pairs. That is, for any (a, b) in the Young Diagram, all (c, d) with c ≤ a and d ≤ b are also in the Young Diagram.
|
YoungDiagram.mem_iff_lt_rowLen
theorem YoungDiagram.mem_iff_lt_rowLen : ∀ {μ : YoungDiagram} {i j : ℕ}, (i, j) ∈ μ ↔ j < μ.rowLen i
This theorem states that for any Young Diagram `μ` and natural numbers `i` and `j`, the pair `(i, j)` is an element in `μ` if and only if `j` is less than the length of the `i`-th row in the Young Diagram `μ`. That is, a pair of natural numbers `(i, j)` belongs to a Young Diagram `μ` precisely when `j` is within the range of the `i`-th row's size or length in `μ`.
More concisely: For any Young Diagram `μ` and natural numbers `i` and `j`, `(i, j) ∈ μ` if and only if `j <` length of the `i`-th row in `μ`.
|
Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.15
theorem Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.15 :
∀ {μ : YoungDiagram} {c : ℕ × ℕ}, (c ∈ μ.transpose) = (c.swap ∈ μ)
This theorem states that for any Young diagram `μ` and any pair of natural numbers `c`, the pair `c` is in the transpose of the Young diagram `μ` if and only if the swapped pair `c` is in `μ`. The transpose of a Young diagram is obtained by swapping each pair of numbers (i.e., swapping the x and y coordinates of each cell), and `Prod.swap` is a function that swaps the elements in a given pair.
More concisely: For any Young diagram `μ` and pair of natural numbers `c`, `c` is in the transpose of `μ` if and only if the swapped pair `(fst c, snd (swap c))` is in `μ`, where `swap` is the function swapping the elements of a pair.
|
YoungDiagram.rowLen_ofRowLens
theorem YoungDiagram.rowLen_ofRowLens :
∀ {w : List ℕ} {hw : List.Sorted (fun x x_1 => x ≥ x_1) w} (i : Fin w.length),
(YoungDiagram.ofRowLens w hw).rowLen ↑i = w.get i
The theorem `YoungDiagram.rowLen_ofRowLens` states that for any list of natural numbers `w` sorted in descending order (i.e., each element is greater than or equal to the next), and any index `i` within the range of the length of `w`, the length of the `i`th row in a Young Diagram constructed from `w` (`YoungDiagram.ofRowLens w hw`) is equal to the `i`th entry of `w`. In other words, the `i`th entry of the sorted list `w` directly determines the length of the corresponding `i`th row in the Young Diagram.
More concisely: For any list of natural numbers `w` in descending order and any index `i` within its length, the length of the `i`th row in the Young Diagram constructed from `w` equals the `i`th element of `w`.
|
YoungDiagram.transpose_transpose
theorem YoungDiagram.transpose_transpose : ∀ (μ : YoungDiagram), μ.transpose.transpose = μ
This theorem states that for any given Young diagram `μ`, the transpose of the transpose of `μ` is equal to `μ` itself. In other words, performing the transpose operation twice on a Young diagram returns the original Young diagram. Here, the transpose operation on a Young diagram involves swapping the coordinates (i's with j's), which corresponds to reflecting the diagram along its main diagonal.
More concisely: The transpose of a Young diagram is equal to its own transpose. In other words, (μ^T)^T = μ for any Young diagram μ.
|
Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.1
theorem Mathlib.Combinatorics.Young.YoungDiagram._auxLemma.1 :
∀ {μ : YoungDiagram} (c : ℕ × ℕ), (c ∈ μ.cells) = (c ∈ μ)
This theorem states that for any Young Diagram `μ` and any pair of natural numbers `c`, the statement that `c` is an element of the cells of `μ` is equivalent to the statement that `c` is an element of `μ`. In other words, being in the set of cells of a Young Diagram is the same as being in the Young Diagram itself. A Young Diagram in this context is a combinatorial structure used in the representation theory of symmetric groups and certain other mathematical entities.
More concisely: For any Young Diagram `μ`, the set of cells in `μ` equals the diagram itself.
|