Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 02:46 3e38b733

View on Github →

feat(analysis/topology): density and continuity lemmas (#292) Still from the perfectoid project

Estimated changes

Modified analysis/topology/continuity.lean

added theorem dense_embedding.closure_image_nhds_of_nhds

added theorem dense_embedding.self_sub_closure_image_preimage_of_open

added theorem dense_embedding.tendsto_vmap_nhds_nhds

Modified analysis/topology/topological_space.lean

added theorem dense_iff_inter_open

added theorem quotient_dense_of_dense