OAI/Combinatorics/Crossing/EvaluationAmbient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zarankiewicz.constrainedInclusion line 11
  2. theorem OAI.Zarankiewicz.constrainedInclusion_eval line 26
  3. def OAI.Zarankiewicz.ambientEval line 35
  4. def OAI.Zarankiewicz.ambientEvalRange line 38
  5. theorem OAI.Zarankiewicz.finrank_ambientEvalRange line 41
  6. theorem OAI.Zarankiewicz.finrank_ambientEvalRange_off_node line 47
  7. theorem OAI.Zarankiewicz.ambientEvalRange_mono_coeff line 53
  8. theorem OAI.Zarankiewicz.ambientEvalRange_le_coeff line 60
  9. theorem OAI.Zarankiewicz.ambientEvalRange_at_node_le line 66