OAI/Combinatorics/SharpRamsey/Selection/EndpointSupports.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.swap line 14
  2. lemma OAI.SharpLogRamsey.Selection.Law.swap_mass line 21
  3. lemma OAI.SharpLogRamsey.Selection.Law.swap_fst line 24
  4. lemma OAI.SharpLogRamsey.Selection.Law.swap_snd line 26
  5. lemma OAI.SharpLogRamsey.Selection.Law.swap_eq_map line 28
  6. lemma OAI.SharpLogRamsey.Selection.entropy_swap line 32
  7. lemma OAI.SharpLogRamsey.Selection.Law.swap_condFst line 36
  8. lemma OAI.SharpLogRamsey.Selection.goodSecond_swap line 41
  9. theorem OAI.SharpLogRamsey.Selection.badFirst_mass line 53
  10. lemma OAI.SharpLogRamsey.Selection.levelSet_card_le_domain line 71
  11. structure OAI.SharpLogRamsey.Selection.AuxiliarySupport line 81
  12. lemma OAI.SharpLogRamsey.Selection.auxiliarySupport_exists line 90
  13. lemma OAI.SharpLogRamsey.Selection.mean_levelLoss_nonneg line 99
  14. theorem OAI.SharpLogRamsey.Selection.reciprocal_auxiliary_choices line 109