OAI/Combinatorics/SharpRamsey/Geometry/Projection.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Projection.rep_mem_line_iff line 16
  2. lemma OAI.SharpLogRamsey.Projection.quotient_rep_ne_zero line 25
  3. def OAI.SharpLogRamsey.Projection.project line 32
  4. lemma OAI.SharpLogRamsey.Projection.quotient_dimension line 36
  5. lemma OAI.SharpLogRamsey.Projection.lift_covector_ne_zero line 40
  6. def OAI.SharpLogRamsey.Projection.projectDual line 48
  7. lemma OAI.SharpLogRamsey.Projection.incident_mk_iff line 54
  8. lemma OAI.SharpLogRamsey.Projection.project_incident_iff line 62
  9. lemma OAI.SharpLogRamsey.Projection.projectDual_injective line 69
  10. lemma OAI.SharpLogRamsey.Projection.collision_center_on_line line 79
  11. lemma OAI.SharpLogRamsey.Projection.joining_line_finrank line 120
  12. lemma OAI.SharpLogRamsey.Projection.joining_line_card line 128
  13. def OAI.SharpLogRamsey.Projection.Collides line 134
  14. lemma OAI.SharpLogRamsey.Projection.collides_on_line line 137
  15. lemma OAI.SharpLogRamsey.Projection.collision_centers_card line 142
  16. def OAI.SharpLogRamsey.Projection.orderedCollisions line 153
  17. theorem OAI.SharpLogRamsey.Projection.collision_total line 156
  18. theorem OAI.SharpLogRamsey.FiniteImage.card_le_image_add_collisions line 178
  19. def OAI.SharpLogRamsey.Projection.projected line 222
  20. lemma OAI.SharpLogRamsey.Projection.noncentral_collision_le line 226
  21. theorem OAI.SharpLogRamsey.Projection.projection_loss line 242
  22. def OAI.SharpLogRamsey.FiniteImage.collisions line 265
  23. lemma OAI.SharpLogRamsey.FiniteImage.collisions_fiber_sum line 268
  24. lemma OAI.SharpLogRamsey.FiniteImage.image_excess_sq line 286
  25. theorem OAI.SharpLogRamsey.FiniteImage.image_excess line 321
  26. lemma OAI.SharpLogRamsey.FiniteImage.collisions_mono line 330
  27. theorem OAI.SharpLogRamsey.FiniteImage.cap_contraction line 337
  28. def OAI.SharpLogRamsey.Projection.liftCap line 359
  29. lemma OAI.SharpLogRamsey.Projection.liftCap_card line 363
  30. lemma OAI.SharpLogRamsey.Projection.mem_liftCap line 368
  31. lemma OAI.SharpLogRamsey.Projection.liftCap_subset line 378
  32. theorem OAI.SharpLogRamsey.Projection.liftCap_contraction line 382
  33. lemma OAI.SharpLogRamsey.Projection.fiber_on_line line 392
  34. lemma OAI.SharpLogRamsey.Projection.project_fiber_card line 409
  35. theorem OAI.SharpLogRamsey.Projection.liftCap_initial line 437