Documentation Verification Report

Montel

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

Statistics

Metric	Count
Definitions `toCompactConvergenceCLM`, `MontelSpace`	2
Theorems `toCompactConvergenceCLM_apply`, `toCompactConvergenceCLM_symm_apply`, `finiteDimensional_of_normedSpace`, `heine_borel`, `isCompact_of_isClosed_of_isVonNBounded`	5
Total	7

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`toCompactConvergenceCLM` 📖	CompOp	2 math math: `toCompactConvergenceCLM_symm_apply`, `toCompactConvergenceCLM_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCompactConvergenceCLM_apply` 📖	mathematical	—	`DFunLike.coe` `CompactConvergenceCLM` `UniformSpace.toTopologicalSpace` `UniformConvergenceCLM.instFunLike` `setOf` `Set` `IsCompact` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `UniformConvergenceCLM.instTopologicalSpace` `UniformConvergenceCLM.instAddCommGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `UniformConvergenceCLM.instModule` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `EquivLike.toFunLike` `equivLike` `toCompactConvergenceCLM` `ContinuousLinearMap.funLike`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`toCompactConvergenceCLM_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `CompactConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `IsCompact` `UniformConvergenceCLM.instAddCommGroup` `ContinuousLinearMap.topologicalSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ContinuousLinearMap.module` `EquivLike.toFunLike` `equivLike` `symm` `toCompactConvergenceCLM` `UniformConvergenceCLM.instFunLike`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`

MontelSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteDimensional_of_normedSpace` 📖	mathematical	—	`FiniteDimensional` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`FiniteDimensional.of_isCompact_closedBall₀` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `isCompact_of_isClosed_of_isVonNBounded` `Metric.isClosed_closedBall` `NormedSpace.isVonNBounded_closedBall`
`heine_borel` 📖	mathematical	`Bornology.IsVonNBounded`	`IsCompact`	—	—
`isCompact_of_isClosed_of_isVonNBounded` 📖	mathematical	`Bornology.IsVonNBounded`	`IsCompact`	—	`heine_borel`

(root)

Definitions

Name	Category	Theorems
`MontelSpace` 📖	CompData	—

---

← Back to Index