Commit 2021-09-10 16:18 574864d3

feat(topology/compact_open): express the compact-open topology as an Inf of topologies (#9106) For f : C(α, β) and a set s in α, define f.restrict s to be the restriction of f as an element of C(s, β). This PR then proves that the compact-open topology on C(α, β) is equal to the infimum of the induced compact-open topologies from the restrictions to compact sets.