Documentation Verification Report

Extension

📁 Source: FLT/Mathlib/MeasureTheory/Haar/Extension.lean

Statistics

Metric	Count
Definitions `IsSES`, `inducedMeasure`, `integrate`, `pullback`, `pushforward`, `IsSES`, `inducedMeasure`, `integrate`, `pullback`, `pushforward`	10
Theorems `apply_apply`, `exact`, `inducedMeasure_lt_of_injOn`, `inducedMeasure_regular`, `integral_inducedMeasure`, `integral_pullback_invFun_apply`, `integrate_apply`, `integrate_mono`, `isAddHaarMeasure_inducedMeasure`, `isClosedEmbedding`, `isOpenQuotientMap`, `not_injOn_of_inducedMeasure_gt`, `not_injOn_of_measure_gt`, `ofClosedAddSubgroup`, `pullback_def`, `pushforward_apply`, `pushforward_def`, `pushforward_mono`, `apply_apply`, `exact`, `inducedMeasure_lt_of_injOn`, `inducedMeasure_regular`, `integral_inducedMeasure`, `integral_pullback_invFun_apply`, `integrate_apply`, `integrate_mono`, `isClosedEmbedding`, `isHaarMeasure_inducedMeasure`, `isOpenQuotientMap`, `not_injOn_of_inducedMeasure_gt`, `not_injOn_of_measure_gt`, `ofClosedSubgroup`, `pullback_def`, `pushforward_apply`, `pushforward_def`, `pushforward_mono`	36
Total	46

TopologicalAddGroup

Definitions

Name	Category	Theorems
`IsSES` 📖	CompData	1 math math: `IsSES.ofClosedAddSubgroup`

TopologicalAddGroup.IsSES

Definitions

Name	Category	Theorems
`inducedMeasure` 📖	CompOp	4 math math: `isAddHaarMeasure_inducedMeasure`, `inducedMeasure_lt_of_injOn`, `integral_inducedMeasure`, `inducedMeasure_regular`
`integrate` 📖	CompOp	3 math math: `integrate_mono`, `integral_inducedMeasure`, `integrate_apply`
`pullback` 📖	CompOp	4 math math: `pushforward_apply`, `integral_pullback_invFun_apply`, `pushforward_def`, `pullback_def`
`pushforward` 📖	CompOp	4 math math: `pushforward_apply`, `pushforward_def`, `pushforward_mono`, `integrate_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_apply` 📖	—	`TopologicalAddGroup.IsSES`	—	—	`exact`
`exact` 📖	—	`TopologicalAddGroup.IsSES`	—	—	—
`inducedMeasure_lt_of_injOn` 📖	mathematical	`TopologicalAddGroup.IsSES`	`inducedMeasure`	—	`inducedMeasure_regular` `integrate_mono` `isOpenQuotientMap` `pushforward_apply` `isClosedEmbedding` `apply_apply`
`inducedMeasure_regular` 📖	mathematical	`TopologicalAddGroup.IsSES`	`inducedMeasure`	—	`integrate_mono`
`integral_inducedMeasure` 📖	mathematical	`TopologicalAddGroup.IsSES`	`inducedMeasure` `integrate`	—	`integrate_mono`
`integral_pullback_invFun_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`pullback`	—	`exact`
`integrate_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`integrate` `pushforward`	—	—
`integrate_mono` 📖	mathematical	`TopologicalAddGroup.IsSES`	`integrate`	—	`pushforward_mono`
`isAddHaarMeasure_inducedMeasure` 📖	mathematical	`TopologicalAddGroup.IsSES`	`inducedMeasure`	—	`integrate_mono` `inducedMeasure_regular` `integral_inducedMeasure` `isOpenQuotientMap` `pushforward_apply` `pushforward_mono` `exact`
`isClosedEmbedding` 📖	—	`TopologicalAddGroup.IsSES`	—	—	—
`isOpenQuotientMap` 📖	—	`TopologicalAddGroup.IsSES`	—	—	—
`not_injOn_of_inducedMeasure_gt` 📖	—	`TopologicalAddGroup.IsSES` `inducedMeasure`	—	—	`inducedMeasure_lt_of_injOn`
`not_injOn_of_measure_gt` 📖	—	—	—	—	`ofClosedAddSubgroup` `isAddHaarMeasure_inducedMeasure` `not_injOn_of_inducedMeasure_gt`
`ofClosedAddSubgroup` 📖	mathematical	—	`TopologicalAddGroup.IsSES`	—	—
`pullback_def` 📖	mathematical	`TopologicalAddGroup.IsSES`	`pullback`	—	—
`pushforward_apply` 📖	mathematical	`TopologicalAddGroup.IsSES`	`pushforward` `pullback`	—	`integral_pullback_invFun_apply`
`pushforward_def` 📖	mathematical	`TopologicalAddGroup.IsSES`	`pushforward` `pullback`	—	—
`pushforward_mono` 📖	mathematical	`TopologicalAddGroup.IsSES`	`pushforward`	—	—

TopologicalGroup

Definitions

Name	Category	Theorems
`IsSES` 📖	CompData	1 math math: `IsSES.ofClosedSubgroup`

TopologicalGroup.IsSES

Definitions

Name	Category	Theorems
`inducedMeasure` 📖	CompOp	4 math math: `inducedMeasure_regular`, `integral_inducedMeasure`, `isHaarMeasure_inducedMeasure`, `inducedMeasure_lt_of_injOn`
`integrate` 📖	CompOp	3 math math: `integral_inducedMeasure`, `integrate_apply`, `integrate_mono`
`pullback` 📖	CompOp	4 math math: `integral_pullback_invFun_apply`, `pullback_def`, `pushforward_def`, `pushforward_apply`
`pushforward` 📖	CompOp	4 math math: `pushforward_def`, `integrate_apply`, `pushforward_apply`, `pushforward_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_apply` 📖	—	`TopologicalGroup.IsSES`	—	—	`exact`
`exact` 📖	—	`TopologicalGroup.IsSES`	—	—	—
`inducedMeasure_lt_of_injOn` 📖	mathematical	`TopologicalGroup.IsSES`	`inducedMeasure`	—	`inducedMeasure_regular` `integrate_mono` `isOpenQuotientMap` `pushforward_apply` `isClosedEmbedding` `apply_apply`
`inducedMeasure_regular` 📖	mathematical	`TopologicalGroup.IsSES`	`inducedMeasure`	—	`integrate_mono`
`integral_inducedMeasure` 📖	mathematical	`TopologicalGroup.IsSES`	`inducedMeasure` `integrate`	—	`integrate_mono`
`integral_pullback_invFun_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`pullback`	—	`exact`
`integrate_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`integrate` `pushforward`	—	—
`integrate_mono` 📖	mathematical	`TopologicalGroup.IsSES`	`integrate`	—	`pushforward_mono`
`isClosedEmbedding` 📖	—	`TopologicalGroup.IsSES`	—	—	—
`isHaarMeasure_inducedMeasure` 📖	mathematical	`TopologicalGroup.IsSES`	`inducedMeasure`	—	`integrate_mono` `inducedMeasure_regular` `integral_inducedMeasure` `isOpenQuotientMap` `pushforward_apply` `pushforward_mono` `exact`
`isOpenQuotientMap` 📖	—	`TopologicalGroup.IsSES`	—	—	—
`not_injOn_of_inducedMeasure_gt` 📖	—	`TopologicalGroup.IsSES` `inducedMeasure`	—	—	`inducedMeasure_lt_of_injOn`
`not_injOn_of_measure_gt` 📖	—	—	—	—	`ofClosedSubgroup` `isHaarMeasure_inducedMeasure` `not_injOn_of_inducedMeasure_gt`
`ofClosedSubgroup` 📖	mathematical	—	`TopologicalGroup.IsSES`	—	—
`pullback_def` 📖	mathematical	`TopologicalGroup.IsSES`	`pullback`	—	—
`pushforward_apply` 📖	mathematical	`TopologicalGroup.IsSES`	`pushforward` `pullback`	—	`integral_pullback_invFun_apply`
`pushforward_def` 📖	mathematical	`TopologicalGroup.IsSES`	`pushforward` `pullback`	—	—
`pushforward_mono` 📖	mathematical	`TopologicalGroup.IsSES`	`pushforward`	—	—

---

← Back to Index