OAI/Geometry/SurfaceImmersion/Whitney/UnorderedSurfacePairs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The Hausdorff space of unordered pairs. The quotient identifies only interchanging the two source points of a double pair.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfacePairSetoid line 11
  2. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.UnorderedSurfacePairs line 28
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair line 30
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_eq line 32
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_swap line 35
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_preimage_image line 38
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_continuous line 52
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_isOpenMap line 55
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_isOpenQuotientMap line 63
  10. instance OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedSurfacePairs_t2 line 67
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unorderedPair_injOn_product line 78