feat: port Topology.MetricSpace.Baire (#3315)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Apr 17, 2023 · 85576cf · 85576cf
1 parent e29b9ea
commit 85576cf
Show file tree

Hide file tree

Showing 2 changed files with 386 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1803,6 +1803,7 @@ import Mathlib.Topology.LocallyFinite
 import Mathlib.Topology.Maps
 import Mathlib.Topology.MetricSpace.Algebra
 import Mathlib.Topology.MetricSpace.Antilipschitz
+import Mathlib.Topology.MetricSpace.Baire
 import Mathlib.Topology.MetricSpace.Basic
 import Mathlib.Topology.MetricSpace.CauSeqFilter
 import Mathlib.Topology.MetricSpace.Completion