Revision #2736 → #3216 · back to history
addedHahn–Banach follows from WKL₀ for separable Banach spaces754309af2a19
addedHahn–Banach theorem for real linear functionals (one-dim step)9bd8d7b492a2
addedContinuous linear functional bounded by continuous seminorm is continuous727ed54af5b7