OAI/Combinatorics/BalancedRyser/Incidence/AffinePairEvaluation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PairEvaluation.eval_intersection line 12
  2. theorem OAI.Balanced.PairEvaluation.intersection_eval line 33
  3. def OAI.Balanced.PairEvaluation.pairEvalEquiv line 57
  4. theorem OAI.Balanced.PairEvaluation.pairEvalEquiv_apply line 63
  5. theorem OAI.Balanced.PairEvaluation.pairEvalEquiv_symm_apply line 66
  6. def OAI.Balanced.PairEvaluation.lineCoordinateEquiv line 69
  7. theorem OAI.Balanced.PairEvaluation.lineCoordinateEquiv_apply line 80
  8. theorem OAI.Balanced.PairEvaluation.existsUnique_eval_pair line 84
  9. theorem OAI.Balanced.PairEvaluation.sum_eval_pair line 93