Documentation Verification Report

AddEquiv

📁 Source: FLT/HaarMeasure/HaarChar/AddEquiv.lean

Statistics

Metric	Count
Definitions `piCongrRight`, `sumCongr`, `piCongrRight`, `prodCongr`	4
Theorems `isAddHaarMeasure_comap`, `isHaarMeasure_comap`, `regular_comap`, `regular_map`, `nnreal_smul`, `nnreal_vadd`, `addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv`, `addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding`, `addEquivAddHaarChar_eq_one_of_compactSpace`, `addEquivAddHaarChar_map_open`, `addEquivAddHaarChar_piCongrRight`, `addEquivAddHaarChar_prodCongr`, `addEquivAddHaarChar_restrictedProductCongrRight`, `addEquivAddHaarChar_restrictedProductCongrRight_of_principal`, `addHaarScalarFactor_map`, `haarScalarFactor_map`, `mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv`, `mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding`, `mulEquivHaarChar_eq_one_of_compactSpace`, `mulEquivHaarChar_map_open`, `mulEquivHaarChar_piCongrRight`, `mulEquivHaarChar_prodCongr`, `mulEquivHaarChar_restrictedProductCongrRight`, `mulEquivHaarChar_restrictedProductCongrRight_of_principal`, `of_isTopologicalAddGroup_of_isOpen_compactSpace_addSubgroup`, `of_isTopologicalGroup_of_isOpen_compactSpace_subgroup`	26
Total	30

ContinuousAddEquiv

Definitions

Name	Category	Theorems
`piCongrRight` 📖	CompOp	1 math math: `MeasureTheory.addEquivAddHaarChar_piCongrRight`
`sumCongr` 📖	CompOp	1 math math: `MeasureTheory.addEquivAddHaarChar_prodCongr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddHaarMeasure_comap` 📖	—	—	—	—	`Topology.IsOpenEmbedding.isAddHaarMeasure_comap`

ContinuousMulEquiv

Definitions

Name	Category	Theorems
`piCongrRight` 📖	CompOp	1 math math: `MeasureTheory.mulEquivHaarChar_piCongrRight`
`prodCongr` 📖	CompOp	1 math math: `MeasureTheory.mulEquivHaarChar_prodCongr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHaarMeasure_comap` 📖	—	—	—	—	`Topology.IsOpenEmbedding.isHaarMeasure_comap`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regular_comap` 📖	—	—	—	—	`Topology.IsOpenEmbedding.regular_comap`
`regular_map` 📖	—	—	—	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` 📖	—	—	—	—	`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding`
`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding` 📖	—	—	—	—	`Topology.IsOpenEmbedding.isAddHaarMeasure_comap` `Topology.IsOpenEmbedding.regular_comap`
`addEquivAddHaarChar_eq_one_of_compactSpace` 📖	—	—	—	—	—
`addEquivAddHaarChar_map_open` 📖	—	—	—	—	`addHaarScalarFactor_map`
`addEquivAddHaarChar_piCongrRight` 📖	mathematical	—	`ContinuousAddEquiv.piCongrRight`	—	`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv` `addEquivAddHaarChar_eq_one_of_compactSpace` `addEquivAddHaarChar_prodCongr`
`addEquivAddHaarChar_prodCongr` 📖	mathematical	—	`ContinuousAddEquiv.sumCongr`	—	`addEquivAddHaarChar_map_open`
`addEquivAddHaarChar_restrictedProductCongrRight` 📖	mathematical	—	`instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `ContinuousAddEquiv.restrictedProductCongrRight`	—	`instBorelSpaceRestrictedProduct_fLT` `addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding` `addEquivAddHaarChar_restrictedProductCongrRight_of_principal`
`addEquivAddHaarChar_restrictedProductCongrRight_of_principal` 📖	mathematical	—	`instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `ContinuousAddEquiv.restrictedProductCongrRight`	—	`addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding` `instBorelSpaceRestrictedProduct_fLT` `addEquivAddHaarChar_eq_one_of_compactSpace` `addEquivAddHaarChar_prodCongr` `addEquivAddHaarChar_piCongrRight`
`addHaarScalarFactor_map` 📖	—	—	—	—	—
`haarScalarFactor_map` 📖	—	—	—	—	—
`mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv` 📖	—	—	—	—	`mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding`
`mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding` 📖	—	—	—	—	`Topology.IsOpenEmbedding.isHaarMeasure_comap` `Topology.IsOpenEmbedding.regular_comap`
`mulEquivHaarChar_eq_one_of_compactSpace` 📖	—	—	—	—	—
`mulEquivHaarChar_map_open` 📖	—	—	—	—	`haarScalarFactor_map`
`mulEquivHaarChar_piCongrRight` 📖	mathematical	—	`ContinuousMulEquiv.piCongrRight`	—	`mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv` `mulEquivHaarChar_eq_one_of_compactSpace` `mulEquivHaarChar_prodCongr`
`mulEquivHaarChar_prodCongr` 📖	mathematical	—	`ContinuousMulEquiv.prodCongr`	—	`mulEquivHaarChar_map_open`
`mulEquivHaarChar_restrictedProductCongrRight` 📖	mathematical	—	`instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `ContinuousMulEquiv.restrictedProductCongrRight`	—	`instBorelSpaceRestrictedProduct_fLT` `mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding` `mulEquivHaarChar_restrictedProductCongrRight_of_principal`
`mulEquivHaarChar_restrictedProductCongrRight_of_principal` 📖	mathematical	—	`instMeasurableSpaceRestrictedProduct_fLT` `instBorelSpaceRestrictedProduct_fLT` `ContinuousMulEquiv.restrictedProductCongrRight`	—	`mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding` `instBorelSpaceRestrictedProduct_fLT` `mulEquivHaarChar_eq_one_of_compactSpace` `mulEquivHaarChar_prodCongr` `mulEquivHaarChar_piCongrRight`

MeasureTheory.IsHaarMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nnreal_smul` 📖	—	—	—	—	—
`nnreal_vadd` 📖	—	—	—	—	—

WeaklyLocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isTopologicalAddGroup_of_isOpen_compactSpace_addSubgroup` 📖	—	—	—	—	—
`of_isTopologicalGroup_of_isOpen_compactSpace_subgroup` 📖	—	—	—	—	—

---

← Back to Index