OAI/Computability/PerfectCompleteness/Foundations/ProjectedCardinality.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ProjectedCardinality.projectedSlots line 16
  2. theorem OAI.PerfectCompleteness.ProjectedCardinality.projected_leaf_domain line 20
  3. def OAI.PerfectCompleteness.ProjectedCardinality.Factor line 24
  4. instance OAI.PerfectCompleteness.ProjectedCardinality.factorFinite line 27
  5. instance OAI.PerfectCompleteness.ProjectedCardinality.factorFintype line 31
  6. instance OAI.PerfectCompleteness.ProjectedCardinality.factorDecidableEq line 35
  7. def OAI.PerfectCompleteness.ProjectedCardinality.factorZero line 39
  8. instance OAI.PerfectCompleteness.ProjectedCardinality.factorNonempty line 47
  9. def OAI.PerfectCompleteness.ProjectedCardinality.factorEquiv line 51
  10. theorem OAI.PerfectCompleteness.ProjectedCardinality.factor_card_eq line 56
  11. def OAI.PerfectCompleteness.ProjectedCardinality.shapeCardinality line 66
  12. theorem OAI.PerfectCompleteness.ProjectedCardinality.shapeCardinality_pos line 71
  13. abbrev OAI.PerfectCompleteness.ProjectedCardinality.Factors line 76
  14. theorem OAI.PerfectCompleteness.ProjectedCardinality.factors_same_cardinality line 79
  15. theorem OAI.PerfectCompleteness.ProjectedCardinality.projected_tree_clean_probability line 84
  16. theorem OAI.PerfectCompleteness.ProjectedCardinality.shape_zero_probability_pos line 96