OAI/Analysis/Steinitz/Transference.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Positive-forward and negative-reverse permutation transference.

  1. def OAI.EuclideanSteinitzBergstrom.walkPrefix line 11
  2. lemma OAI.EuclideanSteinitzBergstrom.sum_take_ofFn line 18
  3. lemma OAI.EuclideanSteinitzBergstrom.take_filter_eq_filter_take line 34
  4. def OAI.EuclideanSteinitzBergstrom.signedOrder line 48
  5. lemma OAI.EuclideanSteinitzBergstrom.signedOrder_perm line 51
  6. lemma OAI.EuclideanSteinitzBergstrom.signedOrder_prefix line 56
  7. lemma OAI.EuclideanSteinitzBergstrom.signed_parts line 84
  8. lemma OAI.EuclideanSteinitzBergstrom.signedOrder_prefix_bound line 95
  9. lemma OAI.EuclideanSteinitzBergstrom.exists_perm_of_list_perm line 120
  10. theorem OAI.EuclideanSteinitzBergstrom.signing_implies_ordering line 133