Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mem_residual

Modification history

2022-06-06 20:46

src/topology/metric_space/baire.lean

refactor(../metric_space/baire): add baire_space class and instances (#14547) …

Modified mem_residual View on Github →

2020-10-13 21:59

src/topology/metric_space/baire.lean

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

Modified mem_residual View on Github →

2020-06-23 17:15

src/topology/metric_space/baire.lean

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

Added mem_residual View on Github →