OAI/Combinatorics/IndependentSets/Repetition/Reindexing.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.reindexEquivline 14 - theorem
OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.pushforward_equivline 20 - theorem
OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.table_const_reindexline 38 - theorem
OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.iid_reindexline 51 - theorem
OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_reindex_of_weightline 62 - def
OAI.IndependentSetsGames.Foundations.Games.Game.questionReindexEquivline 81 - def
OAI.IndependentSetsGames.Foundations.Games.Game.reindexStrategyline 86 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.repetition_question_weight_reindexline 92 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.repetition_questions_reindexline 103 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.coordinateWin_reindexline 116 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.selectedWins_reindexline 134 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.selectedSuccess_reindexline 154 - theorem
OAI.IndependentSetsGames.Foundations.Games.Game.repetition_success_reindexline 169