OAI/Probability/SwitchChain/PairEqualityUnorderedSum.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem315.PairEquality.projection_diag_rightline 14 - theorem
OAI.Problem315.PairEquality.sum_pairProjection_eq_half_orderedline 36 - theorem
OAI.Problem315.PairEquality.sum_disjoint_pairProjection_eq_half_orderedline 54 - theorem
OAI.Problem315.PairEquality.sum_pairProjection_eq_half_fullline 63