LocallyConvex

📁 Source: Mathlib/Topology/ContinuousMap/LocallyConvex.lean

Statistics

Metric	Count
Definitions	0
Theorems instLocallyConvexSpace	1
Total	1

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLocallyConvexSpace 📖	mathematical	—	LocallyConvexSpace ContinuousMap instAddCommMonoidOfContinuousAdd AddCommGroup.toAddCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module compactOpen	—	LocallyConvexSpace.ofBasisZero IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup Filter.HasBasis.nhds_continuousMapConst LocallyConvexSpace.convex_basis_zero

---

← Back to Index