clarify docs

leanprover-community · Jan 10, 2025 · aeed48e · aeed48e
1 parent 6f6ccb9
commit aeed48e
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Mathlib/Order/CompleteLattice/SetLike.lean b/Mathlib/Order/CompleteLattice/SetLike.lean
@@ -6,10 +6,10 @@ Authors: Sven Manthe
 import Mathlib.Order.CompleteSublattice
 
 /-!
-# `SetLike` instance for `CompleteSublattice (Set X)`
+# `SetLike` instance for elements of `CompleteSublattice (Set X)`
 
-This file defines a `SetLike` instance for `CompleteSublattice (Set X)`, but does not register it
-for typeclass inference to avoid conflicts.
+This file defines a `SetLike` instance for elements of `CompleteSublattice (Set X)`, but does not
+register it for typeclass inference to avoid conflicts.
 -/
 
 namespace CompleteSublattice