OAI/Probability/SwitchChain/PairEqualityLocalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.PairEquality.gatedCentered line 13
2. theorem OAI.Problem315.PairEquality.gatedCentered_mem line 16
3. theorem OAI.Problem315.PairEquality.restrictCell_mem line 24

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

4. theorem OAI.Problem315.PairEquality.fiberCell_invariant line 36
5. def OAI.Problem315.PairEquality.localizedVector line 41
6. theorem OAI.Problem315.PairEquality.localizedVector_mem line 44
7. theorem OAI.Problem315.PairEquality.restrict_eq_smul_localizedVector line 49
8. theorem OAI.Problem315.PairEquality.projection_localization line 65