OAI/Dynamics/StandardMap/ShapeTopology.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.locallyAffineSet line 11
  2. def OAI.StandardMapEntropy.locallyUnitSet line 12
  3. lemma OAI.StandardMapEntropy.isOpen_locallyAffineSet line 13
  4. lemma OAI.StandardMapEntropy.isOpen_locallyUnitSet line 17
  5. lemma OAI.StandardMapEntropy.affineOn_closure line 21
  6. lemma OAI.StandardMapEntropy.affineOn_local line 32
  7. lemma OAI.StandardMapEntropy.closure_component_inter_open line 36
  8. lemma OAI.StandardMapEntropy.frontier_component_not_mem line 45
  9. lemma OAI.StandardMapEntropy.open_nonempty_inf_frontier line 50
  10. lemma OAI.StandardMapEntropy.open_nonempty_sup_frontier line 59
  11. lemma OAI.StandardMapEntropy.open_inf_lt_mem line 68
  12. lemma OAI.StandardMapEntropy.open_mem_lt_sup line 74
  13. lemma OAI.StandardMapEntropy.ordConnected_eq_univ_of_unbounded line 80
  14. lemma OAI.StandardMapEntropy.open_ordConnected_eq_Ioi line 87
  15. lemma OAI.StandardMapEntropy.open_ordConnected_eq_Iio line 95