Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient_dense_of_dense

Modification history

2020-10-13 21:59
src/topology/constructions.lean
refactor(*): migrate to `dense` API (#4447) …
Deleted quotient_dense_of_denseView on Github →
2019-10-12 20:07
src/topology/constructions.lean
refactor(topology): mild reorganization (#1541) …
Modified quotient_dense_of_denseView on Github →
2019-03-03 19:05
src/topology/basic.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Modified quotient_dense_of_denseView on Github →
2018-09-21 17:46
analysis/topology/topological_space.lean
feat(analysis/topology, order/filter): theorems for the applicative structure on filter; add list topology
Modified quotient_dense_of_denseView on Github →
2018-08-29 02:46
analysis/topology/topological_space.lean
feat(analysis/topology): density and continuity lemmas (#292) …
Added quotient_dense_of_denseView on Github →