OAI/Probability/BinarySweep/YoungTheory/YoungFinite.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.BinaryCoordinateSweeps.Young.PartitionSpaceline 13 - def
OAI.BinaryCoordinateSweeps.Young.partitionRepline 15 - instance
OAI.BinaryCoordinateSweeps.Young.(instance at line 19)line 19 - lemma
OAI.BinaryCoordinateSweeps.Young.partitionRep_applyline 24 - lemma
OAI.BinaryCoordinateSweeps.Young.partitionRep_equiv_injectiveline 28