Skip to content

Commit

Permalink
correct small typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@StevenClontz @PatrickMassot
StevenClontz authored and PatrickMassot committed May 2, 2024
1 parent bb0b8fb commit a9ae267
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion MIL/C09_Topology/S02_Metric_Spaces.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Convergence and continuity
Using distance functions, we can already define convergent sequences and continuous functions between metric spaces.
They are actually defined in a more general setting covered in the next section,
but we have lemmas recasting the definition is terms of distances.
but we have lemmas recasting the definition in terms of distances.
BOTH: -/
-- QUOTE:
example {u : ℕ → X} {a : X} :
Expand Down

0 comments on commit a9ae267

Please sign in to comment.