Revision #2830 → #3335 · back to history
modifiedLocally convex topological vector spaceef1e0a803d48
| Field | From #2830 | To #3335 |
|---|
| note | The class `LocallyConvexSpace 𝕜 E` asserts that the nhds filter of every point has a basis of convex sets. | The class `LocallyConvexSpace 𝕜 E` asserts the nhds filter of every point has a basis of convex sets. |
addedTranslation invariance of TVS topology7628f5f3a1a7
modifiedStar-shapedness of convex sets containing origincc20d7323417
| Field | From #2830 | To #3335 |
|---|
| moderation_proposal.fields | — | {"mathlib":{"decl":"Convex.starConvex","module":"Mathlib.Analysis.Convex.Basic","match_kind":"exact"}} |
| moderation_proposal.reason | — | `decl_exists` confirms `Convex.starConvex` lives in `Mathlib.Analysis.Convex.Basic`, not `Mathlib.Analysis.Convex.Star`. |
modifiedBalanced setfefe302e3a04
| Field | From #2830 | To #3335 |
|---|
| mathlib.module | Mathlib.Analysis.LocallyConvex.Balanced.Basic | Mathlib.Analysis.LocallyConvex.Basic |
addedLocally convex space is a uniform spacea9d6752ffc5e