OAI/Combinatorics/BalancedRyser/Local/AlignedFreeCoordinates.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.AlignedListProbability.card_alignedPartialOffsets_eqline 13 - def
OAI.Balanced.AlignedListProbability.alignedFreeCoordinatesEquivline 40 - theorem
OAI.Balanced.AlignedListProbability.card_freePositions_of_smallline 51 - theorem
OAI.Balanced.AlignedListProbability.alignedPartial_supportedline 57 - theorem
OAI.Balanced.AlignedListProbability.alignedPartial_conditional_lawline 67 - theorem
OAI.Balanced.AlignedListProbability.alignedPartial_generated_freeline 87 - theorem
OAI.Balanced.AlignedListProbability.alignedPartial_position_old_leftline 104 - theorem
OAI.Balanced.AlignedListProbability.alignedPartial_position_old_rightline 120