OAI/Probability/SwitchChain/PairEqualityUnordered.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.PairEquality.equalitySpace_eq_bot_of_inactive line 13
  2. theorem OAI.Problem315.PairEquality.projection_eq_zero_of_not_disjoint line 26
  3. theorem OAI.Problem315.PairEquality.exists_pair_endpoints line 44
  4. def OAI.Problem315.PairEquality.endpoints line 49
  5. theorem OAI.Problem315.PairEquality.endpoints_spec line 52
  6. def OAI.Problem315.PairEquality.pairProjection line 57
  7. theorem OAI.Problem315.PairEquality.pairProjection_eq line 65
  8. theorem OAI.Problem315.PairEquality.pairProjection_pair line 79
  9. theorem OAI.Problem315.PairEquality.pairProjection_eq_zero_left line 84
  10. theorem OAI.Problem315.PairEquality.pairProjection_eq_zero_right line 88
  11. theorem OAI.Problem315.PairEquality.pairProjection_eq_zero_of_not_disjoint line 93
  12. theorem OAI.Problem315.PairEquality.sum_pairProjection_norm_sq line 104
  13. theorem OAI.Problem315.PairEquality.pairProjection_idempotent line 115
  14. theorem OAI.Problem315.PairEquality.pairProjection_isSymmetric line 123
  15. theorem OAI.Problem315.PairEquality.inner_pairProjection line 137
  16. theorem OAI.Problem315.PairEquality.sum_pairProjection_energy line 145