Anatole Dedecker

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties

1

We refactor a bit the beginning of the file to define a lower adjoint to the operation sending a filter on `β × β` to the corresponding "filter of uniform...

feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum

2

--- [](https://gitpod.io/from-referrer/)

feat(analysis/convex/topology): minimize import

3

Importing `analysis/normed_space/finite_dimension` was problematic for defining the strong operator topology because this needs quite a few facts about convexity but it has to be defined before `continuous_linear_map.has_op_norm`. --- [![Open in...

--- [](https://gitpod.io/from-referrer/)

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

1

--- - [ ] depends on: #14857 - [ ] depends on: #16052 - [ ] depends on: #16054 [](https://gitpod.io/from-referrer/)

feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence

1

--- - [ ] depends on: #14534 [](https://gitpod.io/from-referrer/)

feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence

1

By definition, the sets `S(V) := {(f, g) | ∀ x, (f x, g x) ∈ V}` for `V∈𝓤 β` form a basis for the uniformity of uniform convergence on...

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence

1

The main theorem is `uniform_convergence_on.has_continuous_smul_induced_of_image_bounded`. As explained in the module docstring, one could get rid of requiring `𝔖` to be nonempty and directed, but the easiest way to get that...

feat(topology/algebra/module/locally_convex): generalize `disjoint.exists_open_convexes` to locally convex spaces

1

--- - [x] depends on: #16747 [](https://gitpod.io/from-referrer/)