mathlib

8d2ae95f - fix(analysis/locally_convex): weaken assumptions for `totally_bounded.is_vonN_bounded` (#15468)

fix(analysis/locally_convex): weaken assumptions for `totally_bounded.is_vonN_bounded` (#15468) The `t3_space` assumption was needed because of `nhds_basis_closed_balanced`, but closedness was never used, and removing the closedness condition allows us to drop the `t3_space` assumption