Commit 2023-01-17 06:52 48024901

chore(analysis/convex/exposed): downgrade imports (#18186) Everything in this file was stated for

[normed_linear_ordered_field 𝕜]

but would have worked for

[topological_space 𝕜] [linear_ordered_ring 𝕜] [order_topology 𝕜]

and I have generalized even further where it was easy.