bounded): add an is_central_scalar instance (#12272)

Commit

3 years ago

chore(topology/continuous_function/bounded): add an is_central_scalar instance (#12272) This is only possible very recently now that `𝕜ᵐᵒᵖ` has a metric space instance.

Author

eric-wieser

Parents

feb54736

mathlib3 f7518dbe - chore(topology/continuous_function/bounded): add an is_central_scalar instance (#12272)

mathlib3
f7518dbe - chore(topology/continuous_function/bounded): add an is_central_scalar instance (#12272)