feat(topology/compact_open): express the compact-open topology as an Inf of topologies

[hrmacbeth]

See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Metrisability.20of.20compact-open.20topology/near/252195570

---

• depends on : [Merged by Bors] - chore(topology/order): relate Sup and Inf of topologies to generate_from #9045

[hrmacbeth]

I made a new PR, #9106, to replace this one, and will close this one once @ocfnash thinks through to confirm my doubts about this one.

In this PR it is established that the compact-open topology is equal to

⨅ (s : set α) (hs : is_compact s),
  topological_space.generate_from {m | ∃ (u : set β) (hu : is_open u), m = {f | f '' s ⊆ u}}

but actually, I think that

topological_space.generate_from {m | ∃ (u : set β) (hu : is_open u), m = {f | f '' s ⊆ u}}

is not the same as the topology of uniform convergence on s? In this topology there would be no "small" neighbourhoods of a function with large range.

The result I prove in the other PR is that the compact-open topology is equal to

⨅ (s : set α) (hs : is_compact s),
  topological_space.induced (λ f, f.restrict s) continuous_map.compact_open

[ocfnash]

I made a new PR, #9106, to replace this one, and will close this one once @ocfnash thinks through to confirm my doubts about this one.

Yes I think you're right, though I admit I'm only looking at this from a formal point of view.

I suppose the point is that life will be easiest if we can express the topology as an Inf over compact subsets of K ⊆ α and furthermore that each component in the Inf is the same topology that K gets when regarded as a topological space in its own right (i.e., exactly what you prove in #9106).

I guess that way, if we take the same approach for the uniform structures we should be able to prove is_open_uniformity one K at a time (via https://leanprover-community.github.io/mathlib_docs/topology/uniform_space/basic.html#to_topological_space_Inf).

Of course, unlike this PR, #9106 no longer provides an alternate definition so in a way both are valuable. Similar remarks apply to the uniform structure (assuming I've got the above correct).

Finally I should say that it is likely to be a couple of weeks till I get back to this: I'm going on holiday for 11 days tomorrow and I'm still pushing to get some last bits about convexity finished before I head off. It's a shame because I'm excited to see your work on this but we'll definitely get there.