Krein–Smulian Theorem

Stream: Is there code for X?

[Christopher Hoskin]

Is there a mathlib proof of the Krein–Smulian theorem:

Let X be a Banach Space with dual X^* and let A be a convex subset of X^* such that A ∩ {x ∈X^* : ‖x‖ ≤ r} is weak star closed for every r > 0, then A is weak star closed?

Thanks.

[Yaël Dillies]

Pretty sure we do not

[Jireh Loreaux]

I have a proof of this, but I need to clean it up. I'll get around to it sometime in the next several weeks.