We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent fbb59a1 commit b67f317Copy full SHA for b67f317
1 file changed
Mathlib/Topology/Baire/LocallyCompactRegular.lean
@@ -5,9 +5,7 @@ Authors: Damien Thomine
5
-/
6
module
7
8
-public import Mathlib.Topology.GDelta.Basic
9
public import Mathlib.Topology.Sets.Compacts
10
-public import Mathlib.Topology.Baire.Lemmas
11
12
/-!
13
# Second Baire theorem
0 commit comments