chore: fix accidental namespace (leanprover-community#39135)

vihdzp · vihdzp · commit 34d82a7cc54f · 2026-05-10T08:13:42.000Z
These lemmas were added only 5 days ago in leanprover-community#38809, so I didn't bother with deprecations.
diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean
@@ -221,7 +221,7 @@ theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
 
 end PartialOrder
 
-namespace LinearOrder
+section LinearOrder
 variable [LinearOrder α]
 
 theorem dirSupClosedOn_iff_of_linearOrder :
