mathlib
48024901 - chore(analysis/convex/exposed): downgrade imports (#18186)

Commit
3 years ago
chore(analysis/convex/exposed): downgrade imports (#18186) Everything in this file was stated for ```lean [normed_linear_ordered_field 𝕜] ``` but would have worked for ```lean [topological_space 𝕜] [linear_ordered_ring 𝕜] [order_topology 𝕜] ``` and I have generalized even further where it was easy.
Author
Parents
Loading