OAI/Combinatorics/Progressions/Geometry/CoordinateTreeTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Erdos3.CoordinateDecisionTree line 12
  2. inductive OAI.Erdos3.CoordinateDecisionTree.Valid line 20
  3. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.weaken line 29
  4. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.mono line 39
  5. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.congr_assignment line 59
  6. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.preserve_subset line 88
  7. def OAI.Erdos3.CoordinateDecisionTree.trace line 111
  8. theorem OAI.Erdos3.CoordinateDecisionTree.trace_contains line 117
  9. theorem OAI.Erdos3.CoordinateDecisionTree.trace_agrees line 124
  10. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.trace_good line 138
  11. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.trace_card_le line 146