Commit 2021-03-09 02:15 32bd00f1
View on Github →refactor(topology/bounded_continuous_function): structure extending continuous_map (#6521)
Convert bounded_continuous_function
from a subtype to a structure extending continuous_map
, and some minor improvements to @[simp]
lemmas.