Structure dense_embedding
Modification history
2019-10-07 21:52
src/topology/dense_embedding.lean
refactor(topology/dense_embedding): move dense embeddings to new file (#1515)
Modified dense_embeddingView on Github →2019-07-09 20:34
src/topology/maps.lean
refactor(topology/*): define and use dense_inducing (#1193) …
Modified dense_embeddingView on Github →2019-03-03 19:05
src/topology/constructions.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Modified dense_embeddingView on Github →