mathlib

180f4f20 - feat(analysis/locally_convex): locally bounded implies continuous (#16550)

feat(analysis/locally_convex): locally bounded implies continuous (#16550) We prove that locally bounded linear maps are continuous provided the domain is first countable. In the literature this is usually stated with pseudometrizable, but first countable is equivalent.