OAI/Combinatorics/RamseyFive/Geometry/SubspacePointsEquiv.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ProjectiveIncidence.subspacePointsEquiv line 12
  2. theorem OAI.SharpRamseyFive.ProjectiveIncidence.card_subspacePoints line 36
  3. def OAI.SharpRamseyFive.ProjectiveIncidence.Incident line 42
  4. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_iff line 45
  5. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_iff_dualAnnihilator line 50
  6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.card_points_on_hyperplane line 56
  7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.card_hyperplanes_through_point line 65
  8. lemma OAI.SharpRamseyFive.ProjectiveIncidence.finrank_sup_points line 76
  9. theorem OAI.SharpRamseyFive.ProjectiveIncidence.card_hyperplanes_through_pair line 94
  10. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine line 109
  11. instance OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.(instance at line 114) line 114
  12. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.finrank_sup line 118
  13. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.card_hyperplanes line 139
  14. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.card_hyperplanes_pair line 154
  15. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.through line 171
  16. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.through_eq_iff line 174
  17. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.through_le_iff line 185
  18. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.inFlat line 195
  19. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.trainingOnLine line 199
  20. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.trainingOnLine_eq_fiber line 205
  21. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.sum_trainingOnLine line 212
  22. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.strength line 224
  23. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.sum_strength line 227
  24. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.inFlat_inf line 236
  25. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.overlap_strength line 242
  26. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.hyperplanesOn line 258
  27. def OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.hyperplanesOnPair line 261
  28. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.card_hyperplanesOn line 265
  29. lemma OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.card_hyperplanesOnPair line 271
  30. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.weighted_one_anchor line 283
  31. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.weighted_two_anchors line 292
  32. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.fresh_anchor_weight line 319
  33. theorem OAI.SharpRamseyFive.ProjectiveIncidence.RadialLine.old_anchor_weight line 328
  34. def OAI.SharpRamseyFive.ProjectiveIncidence.incidenceEntry line 340
  35. def OAI.SharpRamseyFive.ProjectiveIncidence.weightOnHyperplane line 343
  36. lemma OAI.SharpRamseyFive.ProjectiveIncidence.sum_entry line 347
  37. lemma OAI.SharpRamseyFive.ProjectiveIncidence.sum_entry_mul_entry line 356
  38. theorem OAI.SharpRamseyFive.ProjectiveIncidence.sum_weightOnHyperplane line 377