OAI/Geometry/SplitTangent/FiniteOpenMaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Open Maps.

  1. def OAI.FiniteOpenMaps.fiberCard line 15
  2. lemma OAI.FiniteOpenMaps.fiberCard_lower line 18
  3. lemma OAI.FiniteOpenMaps.fiberCard_le_isClosed line 40
  4. def OAI.FiniteOpenMaps.constantCardLocus line 50
  5. lemma OAI.FiniteOpenMaps.constantCardLocus_isOpen line 53
  6. lemma OAI.FiniteOpenMaps.constantCardLocus_dense line 64