OAI/Probability/SpanningForest/FinalFactor.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem336.FinalFactor.ruleline 19 - theorem
OAI.Problem336.FinalFactor.rule_borelline 22 - theorem
OAI.Problem336.FinalFactor.rule_equivariantline 26 - theorem
OAI.Problem336.FinalFactor.rule_eq_sampleline 30 - theorem
OAI.Problem336.FinalFactor.sample_hasLawline 34 - theorem
OAI.Problem336.FinalFactor.worksOnGraphline 47 - theorem
OAI.Problem336.FinalFactor.exists_factorline 56