OAI/NumberTheory/Ostmann/Tree/CycleQuartetActionsSelected.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Ostmann.Tree.CycleQuartet.selectedQuartets_nonempty line 11
  2. theorem OAI.Ostmann.Tree.CycleQuartet.positive_fiber_card line 14
  3. theorem OAI.Ostmann.Tree.CycleQuartet.negative_fiber_card line 20
  4. theorem OAI.Ostmann.Tree.CycleQuartet.local_positive_existsUnique line 24
  5. theorem OAI.Ostmann.Tree.CycleQuartet.local_negative_existsUnique line 34
  6. def OAI.Ostmann.Tree.CycleQuartet.positivePosition line 44
  7. def OAI.Ostmann.Tree.CycleQuartet.negativePosition line 47
  8. theorem OAI.Ostmann.Tree.CycleQuartet.positive_mem_iff line 50
  9. theorem OAI.Ostmann.Tree.CycleQuartet.negative_mem_iff line 55
  10. theorem OAI.Ostmann.Tree.CycleQuartet.positions_distinct line 60
  11. def OAI.Ostmann.Tree.CycleQuartet.twoLeafAct line 68
  12. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_eq_twoLeafAct line 72
  13. theorem OAI.Ostmann.Tree.CycleQuartet.negative_label_mem line 78
  14. theorem OAI.Ostmann.Tree.CycleQuartet.localAct_untouched line 86