# Closures of convex sets in locally convex spaces #

This file contains the standard result that if `E`

is a vector space with two locally convex
topologies, then the closure of a convex set is the same in either topology, provided they have the
same collection of continuous linear functionals. In particular, the weak closure of a convex set
in a locally convex space coincides with the closure in the original topology.
Of course, we phrase this in terms of linear maps between locally convex spaces, rather than
creating two separate topologies on the same space.

If `E`

is a locally convex space over `π`

(with `RCLike π`

), and `s : Set E`

is `β`

-convex, then
the closure of `s`

and the weak closure of `s`

coincide. More precisely, the topological closure
commutes with `toWeakSpace π E`

.

This holds more generally for any linear equivalence `e : E ββ[π] F`

between locally convex spaces
such that precomposition with `e`

and `e.symm`

preserves continuity of linear functionals. See
`LinearEquiv.image_closure_of_convex`

.

If `e : E ββ[π] F`

is a linear map between locally convex spaces, and `f β e`

is continuous
for every continuous linear functional `f : F βL[π] π`

, then `e`

commutes with the closure on
convex sets.

If `e`

is a linear isomorphism between two locally convex spaces, and `e`

induces (via
precomposition) an isomorphism between their continuous duals, then `e`

commutes with the closure
on convex sets.

The hypotheses hold automatically for `e := toWeakSpace π E`

, see `Convex.toWeakSpace_closure`

.

If `e`

is a linear isomorphism between two locally convex spaces, and `e`

induces (via
precomposition) an isomorphism between their continuous duals, then `e`

commutes with the closure
on convex sets.

The hypotheses hold automatically for `e := toWeakSpace π E`

, see `Convex.toWeakSpace_closure`

.