OAI/Combinatorics/BalancedRyser/Local/LocalTiming.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.Timing.earlierTuples line 12
  2. theorem OAI.Balanced.Local.Timing.exists_first_class_use line 15
  3. theorem OAI.Balanced.Local.Timing.mem_earlier_classes_iff_first_use line 33
  4. theorem OAI.Balanced.Local.Timing.exists_first_class_use_timing line 51
  5. def OAI.Balanced.Local.Timing.rootsFirstRank line 65
  6. theorem OAI.Balanced.Local.Timing.rootsFirstRank_injective line 68
  7. theorem OAI.Balanced.Local.Timing.rootsFirstRank_prefix line 75