StrongTopology

📁 Source: Mathlib/Analysis/LocallyConvex/StrongTopology.lean

Statistics

Metric	Count
Definitions	0
Theorems instLocallyConvexSpace, locallyConvexSpace	2
Total	2

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLocallyConvexSpace 📖	mathematical	—	LocallyConvexSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module topologicalSpace	—	UniformConvergenceCLM.locallyConvexSpace Bornology.isVonNBounded_empty directedOn_of_sup_mem Bornology.IsVonNBounded.union

UniformConvergenceCLM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyConvexSpace 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset	LocallyConvexSpace UniformConvergenceCLM AddCommGroup.toAddCommMonoid instAddCommGroup instModule instTopologicalSpace	—	LocallyConvexSpace.ofBasisZero instIsTopologicalAddGroup hasBasis_nhds_zero_of_basis LocallyConvexSpace.convex_basis_zero

---

← Back to Index