Revision #3335 → #3886 · back to history
modifiedSeminorm261258bccc85
| Field | From #3335 | To #3886 |
|---|
| mathlib.module | Mathlib.Analysis.Seminorm | Mathlib.Analysis.Normed.Module.Seminorm.Basic |
modifiedStar-shapedness of convex sets containing origincc20d7323417
| Field | From #3335 | To #3886 |
|---|
| mathlib.module | Mathlib.Analysis.Convex.Star | Mathlib.Analysis.Convex.Basic |
| 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`. | — |
| note | `Convex.starConvex` shows any convex set is star-convex at each of its points (in particular at 0 if `0 ∈ s`). | `Convex.starConvex` shows any convex set is star-convex at each of its points (in particular at 0 if `0 ∈ s`). Module corrected from `Mathlib.Analysis.Convex.Star` per prior moderation proposal. |
addedTopological vector space (TVS)01b9f2fedd8b
addedConvex set71cab6564985
addedAbsolutely convex set (disk)51fe0ba34d50