Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-17 19:31 474004f1

View on Github →

fix(topology/dense_embeddings): tweaks (#1684)

fix(topology/dense_embeddings): tweaks This fixes some small issues with last summer dense embedding refactors. This is preparation for helping with Bochner integration. Some of those fixes are backported from the perfectoid project.
chore(dense_embedding): remove is_closed_property'
Update src/topology/uniform_space/completion.lean
Update src/topology/dense_embedding.lean

Estimated changes

Modified src/topology/dense_embedding.lean

added theorem dense_range.closure_range

added theorem dense_range.induction_on

added theorem dense_range.induction_on₂

added theorem dense_range.induction_on₃

added theorem dense_range.prod

deleted theorem dense_range_iff_closure_eq

added theorem dense_range_iff_closure_range

deleted theorem dense_range_prod

modified theorem is_closed_property2

modified theorem is_closed_property3

Modified src/topology/uniform_space/abstract_completion.lean

Modified src/topology/uniform_space/completion.lean

modified theorem uniform_space.completion.dense

modified theorem uniform_space.completion.dense₂

deleted theorem uniform_space.completion.induction_on₄