OAI/Combinatorics/BalancedRyser/Profiles/LocalMarkedAnchors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.MarkedAnchors.mem_purposefulIndices line 18
  2. theorem OAI.Balanced.Local.MarkedAnchors.mem_purposefulDirections line 24
  3. theorem OAI.Balanced.Local.MarkedAnchors.marked_not_retained line 31
  4. theorem OAI.Balanced.Local.MarkedAnchors.retained_pair_of_marked line 38
  5. theorem OAI.Balanced.Local.MarkedAnchors.retained_mem_piece line 59
  6. theorem OAI.Balanced.Local.MarkedAnchors.ordinary_marked_anchors line 68
  7. theorem OAI.Balanced.Local.MarkedAnchors.unused_marked_anchor line 102
  8. theorem OAI.Balanced.Local.MarkedAnchors.exists_purposeful_endpoint line 131
  9. theorem OAI.Balanced.Local.MarkedAnchors.used_marked_anchor line 140
  10. theorem OAI.Balanced.Local.MarkedAnchors.constituent_ne_target line 173
  11. theorem OAI.Balanced.Local.MarkedAnchors.ordinary_ne_target line 181