mathlib
3d9e7907 - fix(topology/metric_space/cau_seq_filter): remove non-terminal simp (#6401)

Commit

4 years ago

fix(topology/metric_space/cau_seq_filter): remove non-terminal simp (#6401)

Author

gebner

gebner

Parents

Loading