Documentation Verification Report

ProperConstSMul

📁 Source: Mathlib/Topology/Algebra/ProperConstSMul.lean

Statistics

Metric	Count
Definitions `ProperConstSMul`, `ProperConstVAdd`	2
Theorems `preimage_smul`, `preimage_vadd`, `isProperMap_smul`, `isProperMap_vadd`, `instProperConstSMulForall`, `instProperConstSMulOfContinuousConstSMul`, `instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace`, `instProperConstSMulProd`, `instProperConstVAddOfContinuousConstVAdd`, `instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace`, `isProperMap_smul`, `isProperMap_vadd`	12
Total	14

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_smul` 📖	mathematical	`IsCompact`	`Set.preimage`	—	`IsProperMap.isCompact_preimage` `isProperMap_smul`
`preimage_vadd` 📖	mathematical	`IsCompact`	`Set.preimage` `HVAdd.hVAdd` `instHVAdd`	—	`IsProperMap.isCompact_preimage` `isProperMap_vadd`

ProperConstSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_smul` 📖	mathematical	—	`IsProperMap`	—	—

ProperConstVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProperMap_vadd` 📖	mathematical	—	`IsProperMap` `HVAdd.hVAdd` `instHVAdd`	—	—

(root)

Definitions

Name	Category	Theorems
`ProperConstSMul` 📖	CompData	3 math math: `instProperConstSMulOfContinuousConstSMul`, `instProperConstSMulProd`, `instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace`
`ProperConstVAdd` 📖	CompData	2 math math: `instProperConstVAddOfContinuousConstVAdd`, `instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instProperConstSMulForall` 📖	mathematical	`ProperConstSMul`	`Pi.instSMul` `Pi.topologicalSpace`	—	`IsProperMap.pi_map` `isProperMap_smul`
`instProperConstSMulOfContinuousConstSMul` 📖	mathematical	—	`ProperConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.isProperMap`
`instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace` 📖	mathematical	—	`ProperConstSMul`	—	`Continuous.isProperMap` `ContinuousConstSMul.continuous_const_smul`
`instProperConstSMulProd` 📖	mathematical	—	`ProperConstSMul` `Prod.instSMul` `instTopologicalSpaceProd`	—	`IsProperMap.prodMap` `isProperMap_smul`
`instProperConstVAddOfContinuousConstVAdd` 📖	mathematical	—	`ProperConstVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.isProperMap`
`instProperConstVAddOfContinuousConstVAddOfT2SpaceOfCompactSpace` 📖	mathematical	—	`ProperConstVAdd`	—	`Continuous.isProperMap` `ContinuousConstVAdd.continuous_const_vadd`
`isProperMap_smul` 📖	mathematical	—	`IsProperMap`	—	`ProperConstSMul.isProperMap_smul`
`isProperMap_vadd` 📖	mathematical	—	`IsProperMap` `HVAdd.hVAdd` `instHVAdd`	—	`ProperConstVAdd.isProperMap_vadd`

---

← Back to Index