Revision #2115 → #2830 · back to history
modifiedNorm (from seminorm via positive definiteness)71da5105ae61
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] satisfies positive definiteness | satisfies positive definiteness, which states that if |
| provenance | ai-agent1 | ai-moderated |
modifiedNeighborhood basis from saturated familyb8a42fd0b4b8
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] is a saturated family of continuous seminorms that induces the topology | is a saturated family of continuous seminorms that induces the topology |
| provenance | ai-agent1 | ai-moderated |
modifiedMinkowski functional is a seminorm for balanced convex absorbing setsf346eb1df88d
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | From this definition it follows that [MATH] is a seminorm if [MATH] is balanced and convex | From this definition it follows that |
| provenance | ai-agent1 | ai-moderated |
modifiedUncountable-dim space with finest vector topology has HBEP964e725008ad
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] has uncountable dimension and if we endow it with the finest vector topology | has uncountable dimension and if we endow it with the finest vector topology |
| provenance | ai-agent1 | ai-moderated |
modifiedClosure characterization in locally convex space54245543db05
| Field | From #2115 | To #2830 |
|---|
| mathlib.module | Mathlib.Topology.Defs.Filter | Mathlib.Topology.ClusterPt |
modifiedConvexity criterion via Minkowski sumsafeef5696210
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | A subset [MATH] is convex if and only if | if and only if for all positive real |
| provenance | ai-agent1 | ai-moderated |
modifiedStar-shapedness of convex sets containing origincc20d7323417
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] is a convex set that contains the origin then | is star shaped at the origin and for all non-negative real |
| provenance | ai-agent1 | ai-moderated |
modifiedOpen convex subsets via sublinear functionals6b744561d6ff
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | the open convex subsets of [MATH] are exactly those that are of the form | are exactly those that are of the form |
| provenance | ai-agent1 | ai-moderated |
modifiedInterior/closure agreement for convex set with non-empty interior8e5442b58ed9
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] is a convex set with non-empty interior, then the closure of | is a convex set with non-empty interior, then the closure of |
| provenance | ai-agent1 | ai-moderated |
modifiedOpen line segment from interior to closure lies in interior3310ad4e2b99
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | if [MATH] is a convex subset of a TVS | Explicitly, this means that if |
| provenance | ai-agent1 | ai-moderated |
modifiedSeparating a vector from a closed subspace by convex neighborhood2e4947f18806
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] is a closed vector subspace of a (not necessarily Hausdorff) locally convex space | is a closed vector subspace of a (not necessarily Hausdorff) locally convex space |
| provenance | ai-agent1 | ai-moderated |
modifiedClosed convex hull is precompact in Hausdorff LCS3d7bdfeb9510
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | the closed convex hull [MATH] of compact subset [MATH] is not necessarily compact although it is a precompact | is not necessarily compact although it is a precompact |
| provenance | ai-agent1 | ai-moderated |
modifiedConvex combination representation for intersecting convex sets5a6e46d5a2b2
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] and [MATH] are convex subsets of a topological vector space | are convex subsets of a topological vector space |
| provenance | ai-agent1 | ai-moderated |
modifiedConvex balanced hullc4997f316aa6
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | the convex balanced hull of [MATH] denoted by [MATH] is the smallest subset | that is convex and balanced |
| provenance | ai-agent1 | ai-moderated |
modifiedConvex balanced hull equals convex hull of balanced hull3502a117007f
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | The convex balanced hull of [MATH] is equal to the convex hull of the balanced hull | is equal to the convex hull of the balanced hull |
| provenance | ai-agent1 | ai-moderated |
modifiedClosed convex hulls compact implies sum closed convex hull compacte05ddb0570e4
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] are subsets of a TVS [MATH] whose closed convex hulls are compact | whose closed convex hulls are compact |
| provenance | ai-agent1 | ai-moderated |
modifiedCarathéodory's theorem550323fd33d2
| Field | From #2115 | To #2830 |
|---|
| note | `Caratheodory.convexHull_eq_union` expresses Carathéodory: the convex hull equals the union of convex hulls of affine-independent finite subsets. | `convexHull_eq_union` in `Mathlib.Analysis.Convex.Caratheodory` expresses Carathéodory: the convex hull equals the union of convex hulls of affine-independent finite subsets. |
modifiedTrivial (indiscrete) topology as coarsest locally convex TVSc726c57daacd
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | Any vector space [MATH] endowed with the trivial topology | endowed with the trivial topology |
| provenance | ai-agent1 | ai-moderated |
modifiedProperties of the finest locally convex topology4d593419db4f
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | Every linear map from [MATH] into another locally convex TVS is necessarily continuous | into another locally convex TVS is necessarily continuous |
| provenance | ai-agent1 | ai-moderated |
modifiedSpace of real-valued sequences as Fréchet spacecd68a116b597
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | The space [MATH] of real valued sequences with the family of seminorms | of real valued sequences with the family of seminorms |
| provenance | ai-agent1 | ai-moderated |
modifiedWeak topology from collection of linear functionals2e36cf81b69c
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | Given any vector space [MATH] and a collection [MATH] of linear functionals on it | of linear functionals on it |
| provenance | ai-agent1 | ai-moderated |
modifiedSchwartz space60c0d20e8f2f
| Field | From #2115 | To #2830 |
|---|
| mathlib.module | Mathlib.Analysis.Distribution.SchwartzSpace | Mathlib.Analysis.Distribution.SchwartzSpace.Basic |
modifiedLp spaces for 0<p<1 lack local convexitye5ad26a56889
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | The spaces [MATH] for [MATH] are equipped with the F-norm | are equipped with the F-norm |
| provenance | ai-agent1 | ai-moderated |
modifiedContinuity criterion for linear maps via seminorms589c79830dde
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | a linear map [MATH] is continuous if and only if for every | a necessary and sufficient criterion for the continuity of a linear map |
| provenance | ai-agent1 | ai-moderated |
modifiedLinear functional bounded by seminorm criterion36f5f7fa1a94
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If [MATH] is a real or complex vector space, [MATH] is a linear functional on | is a real or complex vector space, |
| provenance | ai-agent1 | ai-moderated |
modifiedExistence of continuous norm implies Hausdorff8227f0706cc4
| Field | From #2115 | To #2830 |
|---|
| anchor.snippet | If there exists a continuous norm on a topological vector space [MATH] then [MATH] is necessarily Hausdorff | If there exists a continuous norm on a topological vector space |
| provenance | ai | ai-moderated |
addedBanach–Alaoglu theoremf240000d497d
addedHahn–Banach theorem (existence of continuous linear functionals)f414f1732cbe
addedBalanced setfefe302e3a04
addedAbsorbent (absorbing) seteb93886ecc6a
addedBornological spacecc0f1c41e775