OAI/Combinatorics/BalancedRyser/Local/LocalAnchorExclusion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.AnchorExclusion.Purposeful line 16
  2. theorem OAI.Balanced.Local.AnchorExclusion.adjacent_generator_ne line 20
  3. theorem OAI.Balanced.Local.AnchorExclusion.prescribedPoint_on_left line 28
  4. theorem OAI.Balanced.Local.AnchorExclusion.prescribedPoint_on_right line 34
  5. theorem OAI.Balanced.Local.AnchorExclusion.purposeful_mem_merged line 39
  6. theorem OAI.Balanced.Local.AnchorExclusion.mem_merged_iff_purposeful_of_used line 51
  7. theorem OAI.Balanced.Local.AnchorExclusion.ordinary_line_no_shared_constituent line 92
  8. theorem OAI.Balanced.Local.AnchorExclusion.class_eq_of_shared_constituents line 112
  9. theorem OAI.Balanced.Local.AnchorExclusion.used_pair_no_self_anchor line 121