OAI/Combinatorics/SharpRamsey/Reciprocal/ReciprocalCurrent.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.tests line 13
  2. def OAI.SharpLogRamsey.Selection.Law.core line 16
  3. theorem OAI.SharpLogRamsey.Selection.Law.mem_core line 20
  4. theorem OAI.SharpLogRamsey.Selection.Law.core_le_test line 34
  5. theorem OAI.SharpLogRamsey.Selection.Law.core_failure_le line 40
  6. theorem OAI.SharpLogRamsey.Selection.Law.event_complement line 84
  7. theorem OAI.SharpLogRamsey.Selection.Law.core_capture line 88
  8. theorem OAI.SharpLogRamsey.Selection.Law.event_gt_le line 100
  9. theorem OAI.SharpLogRamsey.Selection.Law.cores_orthogonal line 114
  10. def OAI.SharpLogRamsey.Incidence.Incident line 149
  11. theorem OAI.SharpLogRamsey.Incidence.incident_iff_submodule line 152
  12. def OAI.SharpLogRamsey.Incidence.projectiveSubmoduleEquiv line 158
  13. theorem OAI.SharpLogRamsey.Selection.card_projective_subspace line 191
  14. theorem OAI.SharpLogRamsey.Selection.Law.subspace_mass_bound line 200
  15. theorem OAI.SharpLogRamsey.Selection.sum_powers_le_twice line 217
  16. theorem OAI.SharpLogRamsey.Selection.Law.subspace_rank_pos line 238
  17. theorem OAI.SharpLogRamsey.Selection.Law.subspace_mass_le_pow line 251
  18. theorem OAI.SharpLogRamsey.Selection.Law.small_atoms line 272
  19. theorem OAI.SharpLogRamsey.Selection.negative_log_part line 283
  20. theorem OAI.SharpLogRamsey.Selection.positive_log_part line 305
  21. theorem OAI.SharpLogRamsey.Selection.Law.heavy_atoms line 320
  22. theorem OAI.SharpLogRamsey.Selection.Law.bad_conditional_mass line 340
  23. def OAI.SharpLogRamsey.Selection.Law.condSnd line 371
  24. lemma OAI.SharpLogRamsey.Selection.Law.fst_mul_condSnd line 374
  25. lemma OAI.SharpLogRamsey.Selection.Law.condSnd_mass line 382
  26. lemma OAI.SharpLogRamsey.Selection.Law.paired_cond_mass line 387
  27. lemma OAI.SharpLogRamsey.Selection.Law.product_disintegration line 397
  28. lemma OAI.SharpLogRamsey.Selection.Law.product_event_disintegration line 414