Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 148aefb

Browse files
committed
docs(topology/dense_embedding): Improve explanation (#18134)
An attempt at improving understandability. Closes #1539
1 parent 4b92a46 commit 148aefb

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/topology/dense_embedding.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ import topology.bases
1515
This file defines three properties of functions:
1616
1717
* `dense_range f` means `f` has dense image;
18-
* `dense_inducing i` means `i` is also `inducing`;
19-
* `dense_embedding e` means `e` is also an `embedding`.
18+
* `dense_inducing i` means `i` is also `inducing`, namely it induces the topology on its codomain;
19+
* `dense_embedding e` means `e` is further an `embedding`, namely it is injective and `inducing`.
2020
2121
The main theorem `continuous_extend` gives a criterion for a function
2222
`f : X → Z` to a T₃ space Z to extend along a dense embedding

0 commit comments

Comments
 (0)