Topological vector spaces

ClassLocal convexity#

A LocallyConvexSpace is a topological semimodule over an ordered semiring in which convex neighborhoods of a point form a neighborhood basis at that point.

LocallyConvexSpace.{u_1, u_2} (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜]
  [AddCommMonoid E] [_root_.Module 𝕜 E] [TopologicalSpace E] : Prop

Sources

• Mathlib documentation: LocallyConvexSpace
• Source of LocallyConvexSpace in Mathlib/Topology/Algebra/Module/LocallyConvex.lean
• Mathlib overview: Analysis › Topological vector spaces

MathlibLocallyConvexSpace

Uses 4 · Used by 4

Statement usesConvex subsets · Filter · Module · Topological space

Used byFundamental Theorem of Integral Calculus · Fundamental theorem of calculus, part 2 · Krein–Milman theorem · Weierstrass polynomial approximation theorem

ClassBornology#

A bornology on a type α is a filter of cobounded sets which contains the cofinite filter. Such spaces are equivalently specified by their bounded sets, see Bornology.ofBounded and Bornology.ext_iff_isBounded

Bornology.{u_4} (α : Type u_4) : Type u_4

Sources

• Mathlib documentation: Bornology
• Source of Bornology in Mathlib/Topology/Bornology/Basic.lean
• Mathlib overview: Analysis › Topological vector spaces

MathlibBornology

Uses 2 · Used by 36

Statement usesFilter · Natural number

Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Leibniz’s Series for Pi · Sum of a Geometric Series · Divergence of the Prime Reciprocal Series · Stirling’s Formula · The Triangle Inequality · Stieltjes measure · Absolutely convergent series in Banach spaces · Completeness of spaces of bounded continuous functions · Norm of a continuous linear map · Topology on a normed vector space · Translation number · Euclidean affine space · Urysohn's lemma · Arzela-Ascoli theorem · Baire theorem · Ball · Metric space · Haar measure on a locally compact Hausdorff group · Uniformly continuous function · Bolzano–Weierstrass theorem (1000+ theorems) · Lebesgue differentiation theorem · Bounded convergence theorem · Hahn decomposition theorem · Vitali covering theorem · Krein–Milman theorem · Poisson limit theorem · Slutsky's theorem · Alternating series · Convergence of \(p\)-series for \(p>1\) · Weierstrass polynomial approximation theorem · Bolzano-Weierstrass theorem (Topology of R) · Completeness of R · Complete metric spaces · Limits of sequences · Path connectedness

InstanceWeak-* topology for dualities#

Mathlib states this as WeakBilin.instTopologicalSpace.

WeakBilin.instTopologicalSpace.{u_2, u_4, u_5} {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5}
  [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [_root_.Module 𝕜 E] [AddCommMonoid F]
  [_root_.Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : TopologicalSpace (WeakBilin B)

Sources

• Mathlib documentation: WeakBilin.instTopologicalSpace
• Source of WeakBilin.instTopologicalSpace in Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean
• Mathlib overview: Analysis › Topological vector spaces

MathlibWeakBilin.instTopologicalSpace

Uses 3 · Used by 1

Statement usesAssociative algebra over a commutative ring · Induced topology · Linear map

Used byBanach–Alaoglu theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.