OAI/Probability/MatroidProphet/Density/Birth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.pathHorizon line 11
  2. lemma OAI.MatroidProphet.activation_add_horizon line 13
  3. lemma OAI.MatroidProphet.exists_nominal_member line 17
  4. def OAI.MatroidProphet.nominalBirth line 24
  5. lemma OAI.MatroidProphet.nominalBirth_mem line 28
  6. lemma OAI.MatroidProphet.nominalBirth_bounds line 33
  7. lemma OAI.MatroidProphet.nominalBirth_not_activation_succ line 46
  8. lemma OAI.MatroidProphet.nominalBirth_range line 59
  9. lemma OAI.MatroidProphet.not_mem_nominal_before_birth line 67
  10. lemma OAI.MatroidProphet.mem_nominal_iff_birth_le line 85
  11. lemma OAI.MatroidProphet.nominalPath_generators line 95