Documentation Verification Report

TopologicalSpace

📁 Source: FLT/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean

Statistics

Metric	Count
Definitions `addUnitsContinuousAddEquivAddUnitsType`, `restrictedProductCongrRight`, `restrictedProductPi`, `restrictedProductPrincipal`, `restrictedProductCongrRight`, `restrictedProductMatrix`, `restrictedProductMatrixUnits`, `restrictedProductPi`, `restrictedProductPrincipal`, `restrictedProductUnits`, `restrictedProductMatrix`, `restrictedProductPi`, `restrictedProductPrincipal`, `restrictedProductProd`, `evalContinuousAddMonoidHom`, `flatten_homeomorph`, `flatten_homeomorph'`, `singleContinuousAddMonoidHom`, `unitsContinuousMulEquivUnitsType`	19
Theorems `restrictedProduct_congrRight`, `restrictedProductPi_apply`, `restrictedProductPi_symm_apply`, `restrictedProductPi_apply`, `restrictedProductPi_symm_apply`, `continuous_restrictedProductPi`, `continuous_restrictedProductPi_symm`, `continuous_restrictedProductProd`, `continuous_restrictedProductProd_symm`, `restrictedProductMatrix_aux`, `restrictedProductMatrix_toEquiv`, `SecondCountableTopology_of_principal`, `flatten_homeomorph'_apply`, `flatten_homeomorph'_symm_apply`, `flatten_homeomorph_apply`, `flatten_homeomorph_symm_apply`, `isOpenMap_of_open_components`, `mem_nhds_iff_of_cofinite`, `mem_nhds_iff_of_principal`, `mem_nhds_of_exists_nhds_of_cofinite`, `secondCountableTopology`, `singleContinuousAddMonoidHom_apply_of_ne`, `singleContinuousAddMonoidHom_apply_same`, `continuous_rng_of_principal_pi`	24
Total	43

AddSubmonoid

Definitions

Name	Category	Theorems
`addUnitsContinuousAddEquivAddUnitsType` 📖	CompOp	—

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProduct_congrRight` 📖	—	—	—	—	—

ContinuousAddEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongrRight` 📖	CompOp	3 math math: `MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight`, `MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight_of_principal`, `FiniteAdeleRing.Aux.f_g_local_global`
`restrictedProductPi` 📖	CompOp	2 math math: `restrictedProductPi_apply`, `restrictedProductPi_symm_apply`
`restrictedProductPrincipal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductPi_apply` 📖	mathematical	—	`restrictedProductPi`	—	—
`restrictedProductPi_symm_apply` 📖	mathematical	—	`restrictedProductPi`	—	—

ContinuousMulEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongrRight` 📖	CompOp	2 math math: `MeasureTheory.mulEquivHaarChar_restrictedProductCongrRight_of_principal`, `MeasureTheory.mulEquivHaarChar_restrictedProductCongrRight`
`restrictedProductMatrix` 📖	CompOp	—
`restrictedProductMatrixUnits` 📖	CompOp	—
`restrictedProductPi` 📖	CompOp	2 math math: `restrictedProductPi_symm_apply`, `restrictedProductPi_apply`
`restrictedProductPrincipal` 📖	CompOp	—
`restrictedProductUnits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductPi_apply` 📖	mathematical	—	`restrictedProductPi`	—	—
`restrictedProductPi_symm_apply` 📖	mathematical	—	`restrictedProductPi`	—	—

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_restrictedProductPi` 📖	mathematical	—	`restrictedProductPi`	—	`Continuous.restrictedProduct_congrRight`
`continuous_restrictedProductPi_symm` 📖	mathematical	—	`restrictedProductPi`	—	`continuous_rng_of_principal_pi`
`continuous_restrictedProductProd` 📖	mathematical	—	`restrictedProductProd`	—	`Continuous.restrictedProduct_congrRight`
`continuous_restrictedProductProd_symm` 📖	mathematical	—	`restrictedProductProd`	—	`continuous_rng_of_principal_pi`

Homeomorph

Definitions

Name	Category	Theorems
`restrictedProductMatrix` 📖	CompOp	1 math math: `restrictedProductMatrix_toEquiv`
`restrictedProductPi` 📖	CompOp	—
`restrictedProductPrincipal` 📖	CompOp	—
`restrictedProductProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductMatrix_aux` 📖	—	—	—	—	—
`restrictedProductMatrix_toEquiv` 📖	mathematical	—	`restrictedProductMatrix` `Equiv.restrictedProductMatrix`	—	—

RestrictedProduct

Definitions

Name	Category	Theorems
`evalContinuousAddMonoidHom` 📖	CompOp	—
`flatten_homeomorph` 📖	CompOp	2 math math: `flatten_homeomorph_apply`, `flatten_homeomorph_symm_apply`
`flatten_homeomorph'` 📖	CompOp	2 math math: `flatten_homeomorph'_symm_apply`, `flatten_homeomorph'_apply`
`singleContinuousAddMonoidHom` 📖	CompOp	2 math math: `singleContinuousAddMonoidHom_apply_of_ne`, `singleContinuousAddMonoidHom_apply_same`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SecondCountableTopology_of_principal` 📖	—	—	—	—	—
`flatten_homeomorph'_apply` 📖	mathematical	—	`flatten_homeomorph'`	—	—
`flatten_homeomorph'_symm_apply` 📖	mathematical	—	`flatten_homeomorph'`	—	—
`flatten_homeomorph_apply` 📖	mathematical	—	`flatten_homeomorph`	—	—
`flatten_homeomorph_symm_apply` 📖	mathematical	—	`flatten_homeomorph`	—	—
`isOpenMap_of_open_components` 📖	—	—	—	—	`mem_nhds_iff_of_cofinite` `mem_nhds_of_exists_nhds_of_cofinite` `components_comp_coe_eq_coe_apply`
`mem_nhds_iff_of_cofinite` 📖	—	—	—	—	`mem_nhds_iff_of_principal` `image_coe_preimage_inclusion_subset` `mem_nhds_of_exists_nhds_of_cofinite`
`mem_nhds_iff_of_principal` 📖	—	—	—	—	—
`mem_nhds_of_exists_nhds_of_cofinite` 📖	—	—	—	—	`mem_nhds_iff_of_principal` `coe_comp_inclusion`
`secondCountableTopology` 📖	—	—	—	—	`TopologicalSpace.secondCountableTopology_of_countable_cover'` `instCountableElemSetSetsCofinite_fLT` `SecondCountableTopology_of_principal`
`singleContinuousAddMonoidHom_apply_of_ne` 📖	mathematical	—	`singleContinuousAddMonoidHom`	—	—
`singleContinuousAddMonoidHom_apply_same` 📖	mathematical	—	`singleContinuousAddMonoidHom`	—	—

Submonoid

Definitions

Name	Category	Theorems
`unitsContinuousMulEquivUnitsType` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_rng_of_principal_pi` 📖	—	—	—	—	—

---

← Back to Index