Revision #3216 → #3738 · back to history
modifiedEvery sublinear function is convex29d0e0575ac0
| Field | From #3216 | To #3738 |
|---|
| mathlib.module | Mathlib.Analysis.Seminorm | Mathlib.Analysis.Normed.Module.Seminorm.Basic |
modifiedContinuous linear functional bounded by continuous seminorm is continuous727ed54af5b7
| Field | From #3216 | To #3738 |
|---|
| anchor.snippet | If [MATH] is a continuous sublinear function that dominates a linear functional | is a continuous sublinear function that dominates a linear functional |
| note | The general 'dominated by a continuous sublinear function ⇒ continuous' statement for TVS-valued linear functionals is not stated as a standalone Mathlib lemma. | The general 'dominated by a continuous sublinear function ⇒ continuous' statement for TVS-valued linear functionals is not stated as a standalone Mathlib lemma. Anchor snippet cleaned to remove [MATH] tokens. |
| provenance | ai | ai-moderated |
addedSeparation of a point from a closed subspace by a continuous functionala31de250aa16
addedHahn–Banach provable from the ultrafilter lemma42c55a228412
addedWeak-topology space with separating dual is Hausdorff and locally convexc809c612bbb7