Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dense_of_mem_residual

Modification history

2023-05-20 16:28
src/topology/metric_space/baire.lean
refactor(topology): fix definition of residual (#18962) …
Modified dense_of_mem_residualView on Github →
2022-06-06 20:46
src/topology/metric_space/baire.lean
refactor(../metric_space/baire): add baire_space class and instances (#14547) …
Modified dense_of_mem_residualView on Github →
2021-10-11 07:59
src/topology/metric_space/baire.lean
feat(number_theory/liouville): Liouville numbers form a dense Gδ set (#9646)
Added dense_of_mem_residualView on Github →