OAI/Analysis/SymmetricDomains/FiniteUnion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Release061.NashPatch line 36
  2. def OAI.Release061.NashPatch.image line 50
  3. lemma OAI.Release061.NashPatch.image_nonempty line 52
  4. lemma OAI.Release061.NashPatch.image_connected line 55
  5. lemma OAI.Release061.NashPatch.image_semialgebraic line 58
  6. lemma OAI.Release061.NashPatch.dim_le line 61
  7. lemma OAI.Release061.NashPatch.image_mem_nhds_of_dim_eq line 65
  8. lemma OAI.Release061.NashPatch.dim_lt_of_empty_interior line 80
  9. def OAI.Release061.NashPatch.identity line 89
  10. def OAI.Release061.NashPatch.restrict line 101
  11. def OAI.Release061.NashPatch.comp line 114
  12. lemma OAI.Release061.NashPatch.comp_image line 130
  13. def OAI.Release061.HasFiniteNashCover line 137
  14. lemma OAI.Release061.HasFiniteNashCover.empty line 143
  15. lemma OAI.Release061.HasFiniteNashCover.patch line 146
  16. lemma OAI.Release061.HasFiniteNashCover.union line 150
  17. lemma OAI.Release061.HasFiniteNashCover.finite_union line 158