Module mathcomp.analysis.topology_theory.function_spaces

# The topology of functions spaces Function spaces have no canonical topology. We develop the theory of several general-purpose function space topologies here. ## Topologies on `U -> V` There is no canonical topology on `U->V` in this library. Mathematically, the right topology usually depends on context. We provide three general options in this file which work for various amounts of structures on the domain and codomain. Topologies we consider are: - Topology of pointwise convergence + requires only a topology on V - Topology of uniform convergence + requires only a uniformity on V - Topology of uniform convergence on subspaces + requires only a uniformity on V - The compact-open topology + requires a topology on U and V if you're looking for the topology of compact convergence, note that it is exactly the compact-open topology via `compact_open_fam_compactP`. To locally assign a topology to `->`, import one of the following modules - ArrowAsProduct assigns the product topology - ArrowAsUniformType assigns the uniform topology - ArrowAsCompactOpen assign the compact-open topology The major results are: - Compactness in the product topology via Tychonoff's - Compactness in the compact convergence topology via Ascoli's - Conditions when the supremum and weak topology commute in products - The compact-open topology is the topopology of compact convergence - Cartesian closedness for the category of locally compact topologies ## Function space notations ``` {uniform` A -> V} == the space U -> V, equipped with the topology of uniform convergence from a set A to V, where V is a uniformType {uniform U -> V} := {uniform` [set: U] -> V} {uniform A, F --> f} == F converges to f in {uniform A -> V} {uniform, F --> f} := {uniform setT, F --> f} prod_topology I T == the topology of pointwise convergence on the dependent space `forall (i:I), T i` arrow_uniform_type U V == the topology of uniform convergence on the type `U -> V` {ptws U -> V} == prod_topology for the non-dependent product separate_points_from_closed f == for a closed set U and point x outside some member of the family f, it sends f_i(x) outside (closure (f_i @` U)) Used together with join_product. join_product f == the function (x => f ^~ x) When the family f separates points from closed sets, join_product is an embedding. {ptws, F --> f} == F converges to f in {ptws U -> V} {family fam, U -> V} == the supremum of {uniform A -> f} for each A in `fam` In particular, {family compact, U -> V} is the topology of compact convergence. {family fam, F --> f} == F converges to f in {family fam, U -> V} {compact_open, U -> V} == compact-open topology {compact_open, F --> f} == F converges to f in {compact_open, U -> V} eval == the evaluation map for continuous functions ``` ## Ascoli's theorem notations ``` equicontinuous W x == the set (W : X -> Y) is equicontinuous at x singletons T := [set [set x] | x in [set: T]] pointwise_precompact W == for each (x : X), the set of images [f x | f in W] is precompact ```