OAI/Computability/StarHeight/Avoidance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GeneralizedStarHeight.FiniteAvoidance.mass line 14
  2. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_nonneg line 18
  3. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_mono line 24
  4. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_empty line 33
  5. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_diff line 37
  6. def OAI.GeneralizedStarHeight.FiniteAvoidance.avoids line 45
  7. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.avoids_empty line 49
  8. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.avoids_antitone line 54
  9. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.avoids_insert line 60
  10. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_avoids_insert line 67
  11. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.avoid_union_lower line 73
  12. theorem OAI.GeneralizedStarHeight.FiniteAvoidance.local_lemma line 106
  13. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_one_eq_card line 187
  14. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.mass_one_univ line 192
  15. def OAI.GeneralizedStarHeight.FiniteAvoidance.probability line 197
  16. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_univ line 200
  17. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_compl line 204
  18. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_eq_of_equiv line 211
  19. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_inter_of_independent line 216
  20. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.nonempty_of_mass_pos line 228
  21. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.local_parameter line 234