Revision #1373 → #2115 · back to history
modifiedLocally convex topological vector spaceef1e0a803d48
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | LocallyConvexSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Algebra.Module.LocallyConvex |
| note | — | The class `LocallyConvexSpace 𝕜 E` asserts that the nhds filter of every point has a basis of convex sets. |
| status | — | formalized |
modifiedFréchet spaced6b137f4a78e
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `FrechetSpace` class exists; the ingredients (`LocallyConvexSpace`, `IsCompletelyMetrizableSpace`) are present but not bundled. |
| status | — | not_formalized |
modifiedLocally convex TVS (via convex sets)871b00c4ab0a
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | LocallyConvexSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Algebra.Module.LocallyConvex |
| note | — | `LocallyConvexSpace` is defined exactly by existence of a convex neighborhood basis at every point. |
| status | — | formalized |
modifiedNeighborhood basis of disks2dbc4c0254b5
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | nhds_hasBasis_absConvex |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.AbsConvex |
| note | — | `nhds_hasBasis_absConvex` shows the 0-neighborhood filter has a basis of absolutely convex (= balanced + convex) sets. |
| status | — | formalized |
modifiedSeminorm261258bccc85
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Seminorm |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Seminorm |
| note | — | `Seminorm 𝕜 E` is a structure extending `AddGroupSeminorm` with absolute homogeneity in `𝕜`. |
| status | — | formalized |
modifiedNorm (from seminorm via positive definiteness)71da5105ae61
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Norm |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.Normed.Group.Defs |
| note | — | Mathlib has `Norm` / `NormedAddCommGroup` (norm with definiteness) but defines them directly, not as a positive-definite `Seminorm`. |
| status | — | formalized |
modifiedBase of seminorms64f1e5561ab3
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | SeminormFamily |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `SeminormFamily` is an indexed family of seminorms; the directedness/finite-sup `base` property is captured by `IsBounded` and `Finset.sup` operations but no `BaseOfSeminorms` predicate is named. |
| status | — | partial |
modifiedLocally convex space (second version, via seminorms)055c923da525
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `WithSeminorms p` asserts the topology is the one generated by the seminorm family `p`; `WithSeminorms.toLocallyConvexSpace` connects to the convex-set definition. |
| status | — | formalized |
modifiedInitial topology induced by seminormsfc63d2c6454c
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | SeminormFamily.moduleFilterBasis |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `SeminormFamily.moduleFilterBasis` and `SeminormFamily.topology` build the canonical TVS topology from a seminorm family; `filter_eq_iInf` shows it is the initial topology. |
| status | — | formalized |
modifiedSubbasis at the origin from seminorm preimagesf9e867ebdc5f
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.hasBasis_zero_ball |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `WithSeminorms.hasBasis_zero_ball` (and `basisSets`) shows the nhds of 0 has a basis of finite intersections of seminorm balls. |
| status | — | formalized |
modifiedBase of continuous seminorms52635516f73e
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.continuous_seminorm |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | Continuity of each seminorm in a `WithSeminorms` family is `WithSeminorms.continuous_seminorm`, but no separate `BaseOfContinuousSeminorms` notion is defined. |
| status | — | partial |
modifiedSaturated family of seminorms94de5533fbb3
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Saturated` predicate for seminorm families is defined in Mathlib. |
| status | — | not_formalized |
modifiedNeighborhood basis from saturated familyb8a42fd0b4b8
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Statement depends on saturated families which Mathlib does not define. |
| status | — | not_formalized |
modifiedFréchet space without continuous norm — equivalence17ecbb9e07d0
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No equivalent characterization of Fréchet spaces without continuous norm is in Mathlib (Fréchet not even defined). |
| status | — | not_formalized |
modifiedNet convergence in locally convex spacea2e8cc4169d5
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.tendsto_nhds |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `WithSeminorms.tendsto_nhds` characterizes convergence of a filter (the filter form of nets) as convergence under each seminorm. |
| status | — | formalized |
modifiedMinkowski functional330b31789990
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | gauge |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Gauge |
| note | — | `gauge s x = sInf { r > 0 | x ∈ r • s }` is the Minkowski functional/gauge of a set. |
| status | — | formalized |
modifiedMinkowski functional is a seminorm for balanced convex absorbing setsf346eb1df88d
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | gaugeSeminorm |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Gauge |
| note | — | `gaugeSeminorm hs₀ hs₁ hs₂ : Seminorm 𝕜 E` packages `gauge s` as a seminorm given balanced/convex/absorbent hypotheses. |
| status | — | formalized |
modifiedAuxiliary normed spaces and Banach disks563ed3b23d27
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `BanachDisk` notion or auxiliary-normed-space construction (the `E_B` subspace) is in Mathlib. |
| status | — | not_formalized |
modifiedFilter base yielding locally convex TVS topologye1a87aacab1a
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | LocallyConvexSpace.ofBases |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Topology.Algebra.Module.LocallyConvex |
| note | — | `LocallyConvexSpace.ofBases` (and `ofBasisZero`) constructs the locally convex topology from a filter base of convex sets. |
| status | — | formalized |
modifiedSeparated/total family of seminorms86f108b4a644
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.separating_iff_T1 |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | Mathlib uses the in-line `∀ x ≠ 0, ∃ i, p i x ≠ 0` separating condition in `WithSeminorms.separating_iff_T1` but does not define a stand-alone `Separating` predicate. |
| status | — | partial |
modifiedHausdorff iff separated family of seminorms5e5fee71aa2e
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.separating_iff_T1 |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `WithSeminorms.separating_iff_T1` gives the equivalence between separating and T₁ (which, on a TVS, is equivalent to Hausdorff). |
| status | — | formalized |
modifiedPseudometrizability via countable family of seminormsb705bba49459
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem of the form `pseudoMetrizable ↔ countable seminorm family` is in Mathlib (general first-countable uniform metrizability exists separately). |
| status | — | not_formalized |
modifiedCauchy net in a locally convex space988775a10099
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Cauchy |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.UniformSpace.Cauchy |
| note | — | `Cauchy` filter on a uniform space generalizes Cauchy nets; LCS-specific characterization via seminorms is not packaged separately. |
| status | — | formalized |
modifiedDirected family of seminormsdfffe8f635bb
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Directed` predicate specialised to seminorm families is defined. |
| status | — | not_formalized |
modifiedEquivalent directed family exists923ffd7d9488
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Not formalized; depends on the missing directed-family concept. |
| status | — | not_formalized |
modifiedSeminormability and normability criteria3fe6a8fb9047
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `Seminormable`/`Normable` class or characterization theorem is in Mathlib. |
| status | — | not_formalized |
modifiedSeminormable iff bounded neighborhood of originc59418551f43
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has `IsVonNBounded` and gauge-as-seminorm constructions, but no Kolmogorov normability theorem statement. |
| status | — | not_formalized |
modifiedExtension property and Hahn-Banach extension property (HBEP)7af74fcab385
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No standalone `ExtensionProperty`/`HBEP` predicate is defined in Mathlib. |
| status | — | not_formalized |
modifiedHahn–Banach implies HBEP for Hausdorff locally convex90e3a93991f7
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Module.Dual.exists_extension_of_le_seminorm |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.HahnBanach |
| note | — | Hahn–Banach for LCS (dominated by a continuous seminorm) is `Module.Dual.exists_extension_of_le_seminorm`; the consequence stated in terms of an explicit HBEP predicate is not packaged. |
| status | — | partial |
modifiedUncountable-dim space with finest vector topology has HBEP964e725008ad
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Neither the finest vector topology construction nor this example is in Mathlib. |
| status | — | not_formalized |
modifiedKalton: complete metrizable TVS with HBEP is locally convex8a9c449b5ba8
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Kalton's theorem is not in Mathlib. |
| status | — | not_formalized |
modifiedClosure characterization in locally convex space54245543db05
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | mem_closure_iff_nhds |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.Defs.Filter |
| note | — | The closure characterization is the general topological `mem_closure_iff_nhds`; in LCS the nhds basis is via seminorm balls (`WithSeminorms.hasBasis_ball`). |
| status | — | formalized |
modifiedHausdorff LCS embeds in product of Banach spacesbd95ce317d94
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No such embedding theorem is in Mathlib. |
| status | — | not_formalized |
modifiedAnderson–Kadec theorembc69589602dc
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Anderson–Kadec is not in Mathlib. |
| status | — | not_formalized |
modifiedConvexity criterion via Minkowski sumsafeef5696210
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | convex_iff_pointwise_add_subset |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Basic |
| note | — | `convex_iff_pointwise_add_subset` characterizes convexity by `a • s + b • s ⊆ s` for `a, b ≥ 0`, `a + b = 1`. |
| status | — | formalized |
modifiedStar-shapedness of convex sets containing origincc20d7323417
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Convex.starConvex |
| mathlib.match_kind | — | exact |
| mathlib.module | — | 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`). |
| status | — | formalized |
modifiedMinkowski sum and scalar multiples of convex sets are convex5e8476956f44
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Convex.add |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Basic |
| note | — | `Convex.add` and `Convex.smul` (same file) give convexity of sums and scalar multiples. |
| status | — | formalized |
modifiedOpen convex subsets via sublinear functionals6b744561d6ff
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has Hahn–Banach separation lemmas but no explicit `{x | μ x < 1}` characterization of all open convex sets. |
| status | — | not_formalized |
modifiedInterior and closure of convex set are convexbd628fb5dc35
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Convex.interior |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Topology |
| note | — | `Convex.interior` and `Convex.closure` show the interior/closure of a convex set in a TVS is convex. |
| status | — | formalized |
modifiedInterior/closure agreement for convex set with non-empty interior8e5442b58ed9
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Convex.closure_interior_eq_closure_of_nonempty_interior |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Topology |
| note | — | Mathlib provides both `Convex.closure_interior_eq_closure_of_nonempty_interior` and `Convex.interior_closure_eq_interior_of_nonempty_interior`. |
| status | — | formalized |
modifiedOpen line segment from interior to closure lies in interior3310ad4e2b99
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Convex.openSegment_interior_closure_subset_interior |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Topology |
| note | — | `Convex.openSegment_interior_closure_subset_interior` (and variants) is exactly this statement. |
| status | — | formalized |
modifiedSeparating a vector from a closed subspace by convex neighborhood2e4947f18806
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | exists_open_convex_of_notMem |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.Algebra.Module.LocallyConvex |
| note | — | `exists_open_convex_of_notMem` separates a point from a closed convex set by a convex open neighborhood, of which the closed-subspace case is a corollary. |
| status | — | partial |
modifiedClosure of convex set invariant under compatible topologiesb4eae753c5ff
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem about compatibility of dual pairings and closures of convex sets is in Mathlib. |
| status | — | not_formalized |
modifiedConvex and disked hull of totally bounded sets are totally bounded9ebc70ede280
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | totallyBounded_convexHull |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.Convex.TotallyBounded |
| note | — | `totallyBounded_convexHull` covers the convex-hull half; the disked (absolutely convex) hull case is not formalized. |
| status | — | partial |
modifiedConvex/disked hull of compact set is compact in complete LCSc8667c0b0cbf
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Only the finite-set case (`Set.Finite.isCompact_convexHull`) is formalized; the compact case in complete LCS is not. |
| status | — | not_formalized |
modifiedConvex hull of bounded set is bounded in LCS92e98cbe7931
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `IsVonNBounded.convexHull` lemma is present in Mathlib. |
| status | — | not_formalized |
modifiedClosed convex hull of compact set is compact in Fréchet spacedd29e7335930
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Fréchet spaces are not formalized; this Mazur-style result is absent. |
| status | — | not_formalized |
modifiedLinear combinations of totally bounded sets are totally bounded86180cad7f84
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `TotallyBounded.add` / `TotallyBounded.smul` lemma in this form is in Mathlib. |
| status | — | not_formalized |
modifiedConvex hull and related hullsfc76f5eda8f2
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | convexHull |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Hull |
| note | — | `convexHull`, `closedConvexHull` (`Mathlib.Analysis.Convex.Topology`), and `absConvexHull` (`Mathlib.Analysis.LocallyConvex.AbsConvex`) cover all the named hulls. |
| status | — | formalized |
modifiedConvex hull of compact set in Hilbert space need not be closed1b8941bffe4a
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No counter-example to closedness of `convexHull` of a compact set in a Hilbert space is recorded. |
| status | — | not_formalized |
modifiedClosed convex hull is precompact in Hausdorff LCS3d7bdfeb9510
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | totallyBounded_convexHull |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.Convex.TotallyBounded |
| note | — | `totallyBounded_convexHull` gives totally-bounded (=precompact) for `convexHull`, from which the closure being precompact follows; not stated as a separate lemma. |
| status | — | partial |
modifiedClosure of convex hull of compact set in quasi-complete LCSd12b11a30932
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Quasi-completeness is not in Mathlib; this Mazur-type result is absent. |
| status | — | not_formalized |
modifiedConvex hull of precompact set is precompact265e94fa2707
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | totallyBounded_convexHull |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.TotallyBounded |
| note | — | `totallyBounded_convexHull` is exactly this statement (totally bounded = precompact). |
| status | — | formalized |
modifiedConvex hull of finite union of compact convex sets is compact3fa334e09f48
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Only `Set.Finite.isCompact_convexHull` (finite point set) is in Mathlib; the finite union of compact convex sets version is not. |
| status | — | not_formalized |
modifiedBipolar theoremdf46c2ad65fe
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | LinearMap.subset_bipolar |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.Polar |
| note | — | Only `LinearMap.subset_bipolar` (`s ⊆ bipolar s`) is in Mathlib; the full equality with the closed absolutely convex hull is not. |
| status | — | partial |
modifiedBalanced hull of convex set need not be convex705944a4f901
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No counter-example or remark about non-convexity of `balancedHull` of a convex set is in Mathlib. |
| status | — | not_formalized |
modifiedConvex combination representation for intersecting convex sets5a6e46d5a2b2
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lemma exactly representing points of `convexHull (s ∪ t)` as convex combinations is recorded in this form. |
| status | — | not_formalized |
modifiedConvex balanced hullc4997f316aa6
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | absConvexHull |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.AbsConvex |
| note | — | `absConvexHull` is the smallest absolutely convex (balanced + convex) set containing `s`. |
| status | — | formalized |
modifiedConvex balanced hull equals convex hull of balanced hull3502a117007f
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | absConvexHull_eq_convexHull_balancedHull |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.AbsConvex |
| note | — | `absConvexHull_eq_convexHull_balancedHull` states `absConvexHull 𝕜 s = convexHull 𝕜 (balancedHull 𝕜 s)`. |
| status | — | formalized |
modifiedClosed convex hulls compact implies sum closed convex hull compacte05ddb0570e4
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lemma about compactness of the closed convex hull of a sum is in Mathlib (only `IsCompact.add`). |
| status | — | not_formalized |
modifiedCarathéodory's theorem550323fd33d2
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | convexHull_eq_union |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Convex.Caratheodory |
| note | — | `Caratheodory.convexHull_eq_union` expresses Carathéodory: the convex hull equals the union of convex hulls of affine-independent finite subsets. |
| status | — | formalized |
modifiedTrivial (indiscrete) topology as coarsest locally convex TVSc726c57daacd
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No explicit example/instance giving the indiscrete topology as an LCS is in Mathlib. |
| status | — | not_formalized |
modifiedFinest locally convex topologyfdd6ba6999d9
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not define the finest locally convex topology on a vector space. |
| status | — | not_formalized |
modifiedProperties of the finest locally convex topology4d593419db4f
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Depends on the missing finest-locally-convex-topology construction. |
| status | — | not_formalized |
modifiedNormed spaces and Banach spaces as locally convexbc9fb795c9d5
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | NormedSpace.toLocallyConvexSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `NormedSpace.toLocallyConvexSpace` (instance, ℝ-version) and `NormedSpace.toLocallyConvexSpace'` give the LCS instance for any normed space. |
| status | — | formalized |
modifiedFréchet spaces as locally convex6ea578f4376c
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Fréchet spaces are not defined in Mathlib. |
| status | — | not_formalized |
modifiedSpace of real-valued sequences as Fréchet spacecd68a116b597
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The `ℝ^ℕ` Fréchet-space example with coordinate seminorms is not packaged in Mathlib. |
| status | — | not_formalized |
modifiedWeak topology from collection of linear functionals2e36cf81b69c
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WeakBilin.locallyConvexSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WeakDual |
| note | — | `WeakBilin.locallyConvexSpace` makes the weak topology induced by a bilinear pairing a `LocallyConvexSpace`. |
| status | — | formalized |
modifiedSchwartz space60c0d20e8f2f
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | SchwartzMap |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.Distribution.SchwartzSpace |
| note | — | `SchwartzMap E F` defines the Schwartz space; its locally convex topology by seminorms is also formalized. |
| status | — | formalized |
modifiedSpace of smooth compactly supported functions / LF space2e921924f890
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The space `D(U)` of smooth compactly supported functions as an LF-space is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedContinuous functions with topology of uniform convergence on compacts666e45452582
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | ContinuousMap.compactOpen |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Topology.CompactOpen |
| note | — | The compact-open topology is in `ContinuousMap.compactOpen`; an explicit `LocallyConvexSpace` instance using suprema-of-seminorm structure is in `Mathlib.Topology.ContinuousMap.LocallyConvex`. |
| status | — | partial |
modifiedLp spaces for 0<p<1 lack local convexitye5ad26a56889
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib defines `MemLp`/`Lp` for `0 < p ≤ ∞` but does not state that for `0 < p < 1` the space fails to be locally convex. |
| status | — | not_formalized |
modifiedSpace of measurable functions with convergence in measurec40a8d115410
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Topology of convergence in measure as a non-locally-convex TVS is not formalized in Mathlib. |
| status | — | not_formalized |
modifiedContinuity criterion for linear maps via seminorms589c79830dde
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Seminorm.continuous_from_bounded |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `Seminorm.continuous_from_bounded` (and `WithSeminorms.continuous_iff_continuous_comp`) gives the seminorm characterization of continuity. |
| status | — | formalized |
modifiedContinuity of linear operator into locally convex TVSd50b8306d728
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | WithSeminorms.continuous_iff_continuous_comp |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.WithSeminorms |
| note | — | `WithSeminorms.continuous_iff_continuous_comp` characterizes continuity of a linear map into an LCS by continuity of each composition with a generating seminorm. |
| status | — | formalized |
modifiedLinear functional bounded by seminorm criterion36f5f7fa1a94
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | Module.Dual.exists_extension_of_le_seminorm |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Analysis.LocallyConvex.HahnBanach |
| note | — | Continuity-from-boundedness for linear functionals follows from `Seminorm.continuous_from_bounded` / `continuous_of_isBounded`; a packaged equivalence specifically for functionals is not separate. |
| status | — | partial |
modifiedContinuity criterion for multilinear mapsee25e4e8e8e2
| Field | From #1373 | To #2115 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | A seminorm continuity criterion for multilinear maps into LCS is not present (only the normed setting via `ContinuousMultilinearMap`). |
| status | — | not_formalized |
addedExistence of continuous norm implies Hausdorff8227f0706cc4
addedContinuous linear functional bounded by continuous seminorm41d34cdcdb50
addedDiscrete topology gives a TVS only on the zero space9d1c2c18ded4
addedSequence space ℓ^p with 0<p<1 is not locally convexf27ada16e09c
addedNon-locally-convex examples have trivial dual68086d77b3e5