Theorems · Inductive type · functional analysis
MontelSpace
(𝕜 : Type u_4) → (E : Type u_5) → [SeminormedRing 𝕜] → [Zero E] → [SMul 𝕜 E] → [TopologicalSpace E] → Prop
A Montel space is a topological vector space that has the Heine-Borel property: every closed and
(von Neumann) bounded set is compact.
Note that we are not requiring that E is a barrelled space, so the usual definition of a Montel
space would be [MontelSpace 𝕜 E] [BarrelledSpace 𝕜 E].
- Defined in
- Mathlib.Analysis.LocallyConvex.Montel
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- SeminormedRingstatement · cited by 446
Cited by8
Results whose statement or proof uses this declaration.
- ContinuousLinearEquiv.toCompactConvergenceCLMstatement and proof · cited by 2
- MontelSpace.heine_borelstatement and proof · cited by 1
- MontelSpace.isCompact_of_isClosed_of_isVonNBoundedstatement and proof · cited by 1
- ContinuousLinearEquiv.toCompactConvergenceCLM_applystatement and proof · cited by 0
- ContinuousLinearEquiv.toCompactConvergenceCLM_symm_applystatement and proof · cited by 0
- MontelSpace.casesOnstatement and proof · cited by 0
- MontelSpace.finiteDimensional_of_normedSpacestatement and proof · cited by 0
- MontelSpace.recOnstatement and proof · cited by 0