UnorderedPairChart.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Away from the diagonal the quotient by interchanging the two points is locally a homeomorphism, using disjoint coordinate neighborhoods.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.unordered_pair_local_chart line 11