Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-02 23:49 7b022774

View on Github →

chore(topology/*): more lemmas about dense/dense_range (#9492)

Estimated changes

Modified src/topology/bases.lean

added theorem dense.exists_countable_dense_subset

Modified src/topology/basic.lean

added theorem dense.dense_range_coe

added theorem dense.exists_mem_open

added theorem dense_range.exists_mem_open

Modified src/topology/dense_embedding.lean

added theorem dense.dense_embedding_coe

added theorem dense_embedding.dense_image

modified def dense_embedding.subtype_emb

added theorem dense_inducing.dense_image

modified structure dense_inducing