OAI/Computability/MatchingCount/RawContraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Raw.outside line 10
  2. def OAI.BinaryMatching.Raw.contractMap line 11
  3. def OAI.BinaryMatching.Raw.contract line 12
  4. def OAI.BinaryMatching.Raw.lift line 16
  5. def OAI.BinaryMatching.Raw.cheaper line 18
  6. lemma OAI.BinaryMatching.Raw.outside_rep line 21
  7. lemma OAI.BinaryMatching.Raw.contractMap_rep line 30
  8. lemma OAI.BinaryMatching.Raw.contract_rep line 35
  9. lemma OAI.BinaryMatching.Raw.lift_rep line 42
  10. lemma OAI.BinaryMatching.Raw.cheaper_rep line 48