Skip to content

Commit 57cb125

Browse files
committed
Update Separation.lean
1 parent c6ba537 commit 57cb125

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Analysis/LocallyConvex/Separation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ assert_not_exists ContinuousLinearMap.hasOpNorm
4141

4242
open Set
4343

44-
open Pointwise TopologicalSpace Metric
44+
open Pointwise
4545

4646
variable {E : Type*} {s t : Set E} {x y : E}
4747

0 commit comments

Comments
 (0)