feat: port Topology.Connected (#1934)

leanprover-community · Feb 2, 2023 · 94459eb · 94459eb
1 parent cc02adc
commit 94459eb
Show file tree

Hide file tree

Showing 4 changed files with 1,612 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -942,6 +942,7 @@ import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Basic
 import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Topology.Bornology.Hom
+import Mathlib.Topology.Connected
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Topology.Inseparable