YoungDiagram

📁 Source: Mathlib/Combinatorics/Young/YoungDiagram.lean

Statistics

Metric	Count
Definitions `YoungDiagram`, `card`, `cells`, `cellsOfRowLens`, `col`, `colLen`, `decidableMem`, `equivListRowLens`, `instDistribLattice`, `instInhabited`, `instMax`, `instMin`, `instOrderBot`, `instPartialOrder`, `instSetLikeProdNat`, `ofRowLens`, `row`, `rowLen`, `rowLens`, `transpose`, `transposeOrderIso`	21
Theorems `cells_bot`, `cells_inf`, `cells_ssubset_iff`, `cells_subset_iff`, `cells_sup`, `coe_bot`, `coe_inf`, `coe_sup`, `colLen_anti`, `colLen_eq_card`, `colLen_transpose`, `col_eq_prod`, `equivListRowLens_apply_coe`, `equivListRowLens_symm_apply`, `exists_notMem_col`, `exists_notMem_row`, `ext`, `ext_iff`, `get_rowLens`, `isLowerSet`, `le_of_transpose_le`, `length_rowLens`, `mem_cells`, `mem_cellsOfRowLens`, `mem_col_iff`, `mem_iff_lt_colLen`, `mem_iff_lt_rowLen`, `mem_inf`, `mem_mk`, `mem_ofRowLens`, `mem_row_iff`, `mem_sup`, `mem_transpose`, `mk_mem_col_iff`, `mk_mem_row_iff`, `notMem_bot`, `ofRowLens_to_rowLens_eq_self`, `pos_of_mem_rowLens`, `rowLen_anti`, `rowLen_eq_card`, `rowLen_ofRowLens`, `rowLen_transpose`, `rowLens_length_ofRowLens`, `rowLens_ofRowLens_eq_self`, `rowLens_sorted`, `row_eq_prod`, `transposeOrderIso_apply`, `transposeOrderIso_symm_apply`, `transpose_eq_iff`, `transpose_eq_iff_eq_transpose`, `transpose_le_iff`, `transpose_mono`, `transpose_transpose`, `up_left_mem`	54
Total	75

YoungDiagram

Definitions

Name	Category	Theorems
`card` 📖	CompOp	—
`cells` 📖	CompOp	9 math math: `cells_bot`, `cells_subset_iff`, `mem_cells`, `ext_iff`, `isLowerSet`, `cells_sup`, `cells_ssubset_iff`, `exists_notMem_col`, `cells_inf`
`cellsOfRowLens` 📖	CompOp	1 math math: `mem_cellsOfRowLens`
`col` 📖	CompOp	4 math math: `mk_mem_col_iff`, `mem_col_iff`, `colLen_eq_card`, `col_eq_prod`
`colLen` 📖	CompOp	7 math math: `length_rowLens`, `mem_iff_lt_colLen`, `colLen_eq_card`, `col_eq_prod`, `colLen_anti`, `colLen_transpose`, `rowLen_transpose`
`decidableMem` 📖	CompOp	1 math math: `SemistandardYoungTableau.highestWeight_apply`
`equivListRowLens` 📖	CompOp	2 math math: `equivListRowLens_apply_coe`, `equivListRowLens_symm_apply`
`instDistribLattice` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	3 math math: `mem_sup`, `cells_sup`, `coe_sup`
`instMin` 📖	CompOp	3 math math: `coe_inf`, `mem_inf`, `cells_inf`
`instOrderBot` 📖	CompOp	3 math math: `cells_bot`, `coe_bot`, `notMem_bot`
`instPartialOrder` 📖	CompOp	8 math math: `cells_bot`, `transposeOrderIso_symm_apply`, `cells_subset_iff`, `coe_bot`, `cells_ssubset_iff`, `transposeOrderIso_apply`, `notMem_bot`, `transpose_le_iff`
`instSetLikeProdNat` 📖	CompOp	18 math math: `mem_row_iff`, `mem_ofRowLens`, `mem_cells`, `coe_bot`, `coe_inf`, `mem_iff_lt_rowLen`, `SemistandardYoungTableau.highestWeight_apply`, `exists_notMem_row`, `mk_mem_col_iff`, `mem_inf`, `mem_iff_lt_colLen`, `mem_col_iff`, `mem_sup`, `coe_sup`, `mem_mk`, `mk_mem_row_iff`, `mem_transpose`, `notMem_bot`
`ofRowLens` 📖	CompOp	6 math math: `mem_ofRowLens`, `ofRowLens_to_rowLens_eq_self`, `rowLen_ofRowLens`, `rowLens_length_ofRowLens`, `rowLens_ofRowLens_eq_self`, `equivListRowLens_symm_apply`
`row` 📖	CompOp	4 math math: `mem_row_iff`, `rowLen_eq_card`, `row_eq_prod`, `mk_mem_row_iff`
`rowLen` 📖	CompOp	8 math math: `mem_iff_lt_rowLen`, `rowLen_eq_card`, `get_rowLens`, `row_eq_prod`, `rowLen_ofRowLens`, `rowLen_anti`, `colLen_transpose`, `rowLen_transpose`
`rowLens` 📖	CompOp	6 math math: `ofRowLens_to_rowLens_eq_self`, `length_rowLens`, `equivListRowLens_apply_coe`, `rowLens_length_ofRowLens`, `rowLens_ofRowLens_eq_self`, `rowLens_sorted`
`transpose` 📖	CompOp	10 math math: `transposeOrderIso_symm_apply`, `transpose_transpose`, `transpose_mono`, `transpose_eq_iff`, `transpose_eq_iff_eq_transpose`, `colLen_transpose`, `rowLen_transpose`, `transposeOrderIso_apply`, `mem_transpose`, `transpose_le_iff`
`transposeOrderIso` 📖	CompOp	2 math math: `transposeOrderIso_symm_apply`, `transposeOrderIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cells_bot` 📖	mathematical	—	`cells` `Bot.bot` `YoungDiagram` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `Finset` `Finset.instEmptyCollection`	—	—
`cells_inf` 📖	mathematical	—	`cells` `YoungDiagram` `instMin` `Finset` `Finset.instInter`	—	—
`cells_ssubset_iff` 📖	mathematical	—	`Finset` `Finset.instHasSSubset` `cells` `YoungDiagram` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`cells_subset_iff` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `cells` `YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`cells_sup` 📖	mathematical	—	`cells` `YoungDiagram` `instMax` `Finset` `Finset.instUnion`	—	—
`coe_bot` 📖	mathematical	—	`SetLike.coe` `YoungDiagram` `instSetLikeProdNat` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot` `Set` `Set.instEmptyCollection`	—	`Set.ext`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `YoungDiagram` `instSetLikeProdNat` `instMin` `Set` `Set.instInter`	—	`Finset.coe_inter`
`coe_sup` 📖	mathematical	—	`SetLike.coe` `YoungDiagram` `instSetLikeProdNat` `instMax` `Set` `Set.instUnion`	—	`Finset.coe_union`
`colLen_anti` 📖	mathematical	—	`colLen`	—	`rowLen_transpose` `rowLen_anti`
`colLen_eq_card` 📖	mathematical	—	`colLen` `Finset.card` `col`	—	`Prod.mk_left_injective` `col_eq_prod` `Finset.product_singleton` `Finset.card_map` `Finset.card_range`
`colLen_transpose` 📖	mathematical	—	`colLen` `transpose` `rowLen`	—	`exists_notMem_row` `exists_notMem_col` `Nat.find.congr_simp`
`col_eq_prod` 📖	mathematical	—	`col` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.range` `colLen` `Finset.instSingleton`	—	`Finset.ext`
`equivListRowLens_apply_coe` 📖	mathematical	—	`List.SortedGE` `Nat.instPreorder` `DFunLike.coe` `Equiv` `YoungDiagram` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivListRowLens` `rowLens`	—	—
`equivListRowLens_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `List.SortedGE` `Nat.instPreorder` `YoungDiagram` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivListRowLens` `ofRowLens`	—	—
`exists_notMem_col` 📖	mathematical	—	`Finset` `Finset.instMembership` `cells`	—	`exists_notMem_row`
`exists_notMem_row` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	`Infinite.exists_notMem_finset` `instInfiniteNat` `Finset.mem_preimage`
`ext` 📖	—	`cells`	—	—	—
`ext_iff` 📖	mathematical	—	`cells`	—	`ext`
`get_rowLens` 📖	mathematical	`rowLens`	`rowLen`	—	—
`isLowerSet` 📖	mathematical	—	`IsLowerSet` `Prod.instLE_mathlib` `SetLike.coe` `Finset` `Finset.instSetLike` `cells`	—	—
`le_of_transpose_le` 📖	—	`YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `transpose`	—	—	—
`length_rowLens` 📖	mathematical	—	`rowLens` `colLen`	—	—
`mem_cells` 📖	mathematical	—	`Finset` `Finset.instMembership` `cells` `YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—
`mem_cellsOfRowLens` 📖	mathematical	—	`Finset` `Finset.instMembership` `cellsOfRowLens`	—	`cellsOfRowLens.eq_1` `instIsEmptyFalse` `Nat.succ_injective` `cellsOfRowLens.eq_2` `Prod.mk_right_injective` `Finset.singleton_product`
`mem_col_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `col` `YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—
`mem_iff_lt_colLen` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `colLen`	—	`rowLen_transpose` `mem_iff_lt_rowLen`
`mem_iff_lt_rowLen` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `rowLen`	—	`exists_notMem_row` `rowLen.eq_1` `Nat.lt_find_iff` `up_left_mem` `le_refl`
`mem_inf` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `instMin`	—	`Finset.mem_inter`
`mem_mk` 📖	mathematical	`IsLowerSet` `Prod.instLE_mathlib` `SetLike.coe` `Finset` `Finset.instSetLike`	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `Finset.instMembership`	—	—
`mem_ofRowLens` 📖	mathematical	`List.SortedGE` `Nat.instPreorder`	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `ofRowLens`	—	`mem_cellsOfRowLens`
`mem_row_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `row` `YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—
`mem_sup` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `instMax`	—	`Finset.mem_union`
`mem_transpose` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `transpose`	—	—
`mk_mem_col_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `col` `YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—
`mk_mem_row_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `row` `YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—
`notMem_bot` 📖	mathematical	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBot`	—	`Finset.notMem_empty`
`ofRowLens_to_rowLens_eq_self` 📖	mathematical	—	`ofRowLens` `rowLens` `rowLens_sorted`	—	`ext` `rowLens_sorted` `Finset.ext` `get_rowLens` `length_rowLens` `LE.le.trans_lt`
`pos_of_mem_rowLens` 📖	—	`rowLens`	—	—	`rowLens.eq_1` `mem_iff_lt_rowLen` `mem_iff_lt_colLen`
`rowLen_anti` 📖	mathematical	—	`rowLen`	—	`lt_self_iff_false` `mem_iff_lt_rowLen` `up_left_mem` `le_refl`
`rowLen_eq_card` 📖	mathematical	—	`rowLen` `Finset.card` `row`	—	`Prod.mk_right_injective` `row_eq_prod` `Finset.singleton_product` `Finset.card_map` `Finset.card_range`
`rowLen_ofRowLens` 📖	mathematical	`List.SortedGE` `Nat.instPreorder`	`rowLen` `ofRowLens`	—	`exists_notMem_row` `Nat.find.congr_simp`
`rowLen_transpose` 📖	mathematical	—	`rowLen` `transpose` `colLen`	—	`exists_notMem_row` `exists_notMem_col` `Nat.find.congr_simp`
`rowLens_length_ofRowLens` 📖	mathematical	`List.SortedGE` `Nat.instPreorder`	`rowLens` `ofRowLens`	—	`exists_notMem_col` `length_rowLens` `Nat.find.congr_simp` `instIsEmptyFalse`
`rowLens_ofRowLens_eq_self` 📖	mathematical	`List.SortedGE` `Nat.instPreorder`	`rowLens` `ofRowLens`	—	`rowLens_length_ofRowLens` `get_rowLens` `rowLen_ofRowLens`
`rowLens_sorted` 📖	mathematical	—	`List.SortedGE` `Nat.instPreorder` `rowLens`	—	`List.Pairwise.sortedGE` `rowLen_anti`
`row_eq_prod` 📖	mathematical	—	`row` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.instSingleton` `Finset.range` `rowLen`	—	`Finset.ext`
`transposeOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `transposeOrderIso` `transpose`	—	—
`transposeOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `transposeOrderIso` `transpose`	—	—
`transpose_eq_iff` 📖	mathematical	—	`transpose`	—	`transpose_eq_iff_eq_transpose` `transpose_transpose`
`transpose_eq_iff_eq_transpose` 📖	mathematical	—	`transpose`	—	`transpose_transpose`
`transpose_le_iff` 📖	mathematical	—	`YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `transpose`	—	`transpose_transpose` `le_of_transpose_le`
`transpose_mono` 📖	mathematical	`YoungDiagram` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`transpose`	—	`transpose_le_iff`
`transpose_transpose` 📖	mathematical	—	`transpose`	—	`ext` `Finset.ext`
`up_left_mem` 📖	—	`YoungDiagram` `SetLike.instMembership` `instSetLikeProdNat`	—	—	`isLowerSet`

(root)

Definitions

Name	Category	Theorems
`YoungDiagram` 📖	CompData	28 math math: `YoungDiagram.cells_bot`, `YoungDiagram.transposeOrderIso_symm_apply`, `YoungDiagram.cells_subset_iff`, `YoungDiagram.mem_row_iff`, `YoungDiagram.mem_ofRowLens`, `YoungDiagram.mem_cells`, `YoungDiagram.coe_bot`, `YoungDiagram.coe_inf`, `YoungDiagram.mem_iff_lt_rowLen`, `SemistandardYoungTableau.highestWeight_apply`, `YoungDiagram.exists_notMem_row`, `YoungDiagram.mk_mem_col_iff`, `YoungDiagram.mem_inf`, `YoungDiagram.mem_iff_lt_colLen`, `YoungDiagram.mem_col_iff`, `YoungDiagram.equivListRowLens_apply_coe`, `YoungDiagram.mem_sup`, `YoungDiagram.cells_sup`, `YoungDiagram.cells_ssubset_iff`, `YoungDiagram.coe_sup`, `YoungDiagram.mem_mk`, `YoungDiagram.mk_mem_row_iff`, `YoungDiagram.equivListRowLens_symm_apply`, `YoungDiagram.transposeOrderIso_apply`, `YoungDiagram.mem_transpose`, `YoungDiagram.notMem_bot`, `YoungDiagram.cells_inf`, `YoungDiagram.transpose_le_iff`

---

← Back to Index