Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dense_inter_of_open_right

Modification history

2020-10-13 21:59

src/topology/basic.lean

refactor(*): migrate to `dense` API (#4447) …

Deleted dense_inter_of_open_right View on Github →

2020-06-23 17:15

src/topology/basic.lean

feat(topology/metric_space/baire): define filter `residual` (#3149) …

Added dense_inter_of_open_right View on Github →