Skip to content

Commit cdca999

Browse files
committed
feat: port Topology.Inseparable (#1908)
1 parent 5098b9f commit cdca999

File tree

2 files changed

+640
-0
lines changed

2 files changed

+640
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -927,6 +927,7 @@ import Mathlib.Topology.Bornology.Constructions
927927
import Mathlib.Topology.Bornology.Hom
928928
import Mathlib.Topology.Constructions
929929
import Mathlib.Topology.ContinuousOn
930+
import Mathlib.Topology.Inseparable
930931
import Mathlib.Topology.LocalExtr
931932
import Mathlib.Topology.LocallyFinite
932933
import Mathlib.Topology.Maps

0 commit comments

Comments
 (0)