Skip to content

Commit

Permalink
doc(topology/dense_embedding): fix list syntax in a comment (leanprov…
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud authored and anrddh committed May 15, 2020
1 parent 78c581e commit 1c67eb3
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/topology/dense_embedding.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ import topology.separation
This file defines three properties of functions:
`dense_range f` means `f` has dense image;
`dense_inducing i` means `i` is also `inducing`;
`dense_embedding e` means `e` is also an `embedding`.
* `dense_range f` means `f` has dense image;
* `dense_inducing i` means `i` is also `inducing`;
* `dense_embedding e` means `e` is also an `embedding`.
The main theorem `continuous_extend` gives a criterion for a function
`f : X → Z` to a regular (T₃) space Z to extend along a dense embedding
Expand Down

0 comments on commit 1c67eb3

Please sign in to comment.