Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 09:01 e5c66a09

View on Github →

chore(topology/continuous_function/bounded): add comp_continuous (#10134)

Estimated changes