doc(Geometry/Manifold): manifolds are not required to be Hausdorff no…

…r second countable (#7159) For many results, these assumptions are not required. As finite-dimensional manifolds are commonly assumed to be Hausdorff and second countable, it seems worth to call this out explicitly.
leanprover-community · Sep 18, 2023 · f8add0e · f8add0e
1 parent 9dd5d67
commit f8add0e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
@@ -25,6 +25,9 @@ With this groupoid at hand and the general machinery of charted spaces, we thus
 of `C^n` manifold with respect to any model with corners `I` on `(E, H)`. We also introduce a
 specific type class for `C^∞` manifolds as these are the most commonly used.
 
+Some texts assume manifolds to be Hausdorff and secound countable. We (in mathlib) assume neither,
+but add these assumptions later as needed. (Quite a few results still do not require them.)
+
 ## Main definitions
 
 * `ModelWithCorners 𝕜 E H` :