Skip to content

Commit 0825c47

Browse files
fix: close namespace
1 parent f66ee80 commit 0825c47

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

Mathlib/Topology/GDelta/CompletelyMetrizable.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,3 +84,5 @@ theorem isGδ {s : Set X} (hs : IsCompletelyMetrizableSpace s) : IsGδ s := by
8484
(continuous_subtype_val.continuousAt.mono_left hy)
8585
rw [hxy]
8686
exact Subtype.coe_prop y
87+
88+
end TopologicalSpace.IsCompletelyMetrizableSpace

0 commit comments

Comments
 (0)