OAI/Probability/SwitchChain/PairEqualityCell.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairEquality.restrictCell_mem line 15

   Distinct definitions of this name: OAI/Probability/SwitchChain/PairEqualityLocalization.lean:24 (same statement text; different proof or body). Qualify references as OAI.Problem315.PairEquality.restrictCell_mem@path.

2. theorem OAI.Problem315.PairEquality.projection_restrictCell line 29
3. theorem OAI.Problem315.PairEquality.projection_restrict_disjointCell_left line 36
4. theorem OAI.Problem315.PairEquality.projection_restrict_disjointCell_right line 44