Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-07 21:52 1bf831f2

View on Github →

refactor(topology/dense_embedding): move dense embeddings to new file (#1515)

Estimated changes

added theorem dense_embedding.mk'
added structure dense_embedding
added theorem dense_inducing.mk'
added structure dense_inducing
added theorem dense_range.comp
added theorem dense_range.nonempty
added def dense_range
deleted theorem dense_embedding.inj_iff
deleted theorem dense_embedding.mk'
deleted structure dense_embedding
deleted theorem dense_inducing.extend_eq
deleted theorem dense_inducing.mk'
deleted structure dense_inducing
deleted theorem dense_range.comp
deleted theorem dense_range.nonempty
deleted def dense_range