OAI/Combinatorics/SharpRamsey/Windows/WindowLayout.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.Selection.Windows.Slot line 11
  2. abbrev OAI.SharpLogRamsey.Selection.Windows.Block line 12
  3. def OAI.SharpLogRamsey.Selection.Windows.quarter line 14
  4. lemma OAI.SharpLogRamsey.Selection.Windows.quarter_injective line 17
  5. def OAI.SharpLogRamsey.Selection.Windows.embedding line 30
  6. def OAI.SharpLogRamsey.Selection.Windows.owner line 40
  7. lemma OAI.SharpLogRamsey.Selection.Windows.embedding_owner line 44
  8. def OAI.SharpLogRamsey.Selection.Windows.middle line 55
  9. lemma OAI.SharpLogRamsey.Selection.Windows.middle_unowned line 64
  10. def OAI.SharpLogRamsey.Selection.Windows.position line 70
  11. lemma OAI.SharpLogRamsey.Selection.Windows.position_injective line 72
  12. lemma OAI.SharpLogRamsey.Selection.Windows.between line 87
  13. lemma OAI.SharpLogRamsey.Selection.Windows.before_next line 94
  14. lemma OAI.SharpLogRamsey.Selection.Windows.middle_card line 102