OAI/Probability/MatroidProphet/Density/Basic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.natRank line 13
  2. lemma OAI.MatroidProphet.rank_ne_top line 16
  3. lemma OAI.MatroidProphet.natRank_mono line 19
  4. lemma OAI.MatroidProphet.natRank_closure line 24
  5. lemma OAI.MatroidProphet.natRank_empty line 29
  6. lemma OAI.MatroidProphet.natRank_submod line 32
  7. lemma OAI.MatroidProphet.flat_inter line 39
  8. def OAI.MatroidProphet.densityObjective line 47
  9. lemma OAI.MatroidProphet.densityObjective_supermod line 50
  10. def OAI.MatroidProphet.IsDensityMax line 69
  11. lemma OAI.MatroidProphet.exists_densityMax line 73
  12. lemma OAI.MatroidProphet.densityMax_union line 79
  13. lemma OAI.MatroidProphet.exists_largest_densityMax line 93
  14. def OAI.MatroidProphet.densityExpansion line 109
  15. lemma OAI.MatroidProphet.densityExpansion_spec line 113
  16. lemma OAI.MatroidProphet.densityExpansion_extensive line 119
  17. lemma OAI.MatroidProphet.densityExpansion_flat line 123
  18. lemma OAI.MatroidProphet.densityExpansion_mono line 127
  19. lemma OAI.MatroidProphet.densityExpansion_residual line 147
  20. lemma OAI.MatroidProphet.natRank_eq_ncard_of_basis line 170
  21. lemma OAI.MatroidProphet.closure_eq_of_subset_of_natRank_le line 174
  22. lemma OAI.MatroidProphet.densityExpansion_generated line 180
  23. lemma OAI.MatroidProphet.exists_extension_generators line 204
  24. lemma OAI.MatroidProphet.densityExpansion_generator_step line 236