Skip to content

Commit 898eace

Browse files
committed
chore(Topology/Connected/LocPathConnected): fix typo in LocPathConnectedSpace docstring (leanprover-community#38327)
This PR fixes a small typo in the docstring of `LocPathConnectedSpace`: the sentence was missing the word "if". 🤖 Prepared with Claude Code
1 parent 1c558eb commit 898eace

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Topology/Connected/LocPathConnected.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {x y z : X} {ι
5050

5151
section LocPathConnectedSpace
5252

53-
/-- A topological space is locally path connected, at every point, path connected
53+
/-- A topological space is locally path connected if, at every point, path connected
5454
neighborhoods form a neighborhood basis. -/
5555
class LocPathConnectedSpace (X : Type*) [TopologicalSpace X] : Prop where
5656
/-- Each neighborhood filter has a basis of path-connected neighborhoods. -/

0 commit comments

Comments
 (0)