Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_sum_dom

Modification history

2023-02-26 22:16
src/topology/constructions.lean
refactor(topology/metric_space): drop `dist_setoid` (#18502) …
Added continuous_sum_domView on Github →