Documentation Verification Report

Product

📁 Source: Mathlib/Topology/Category/Profinite/Product.lean

Statistics

Metric	Count
Definitions `map`, `obj`, `π_app`, `asLimitindexConeIso`, `indexCone`, `indexCone_isLimit`, `indexFunctor`, `isoindexConeLift`	8
Theorems `eq_of_forall_π_app_eq`, `map_comp_π_app`, `surjective_π_app`, `isIso_indexCone_lift`	4
Total	12

Profinite

Definitions

Name	Category	Theorems
`asLimitindexConeIso` 📖	CompOp	—
`indexCone` 📖	CompOp	1 math math: `isIso_indexCone_lift`
`indexCone_isLimit` 📖	CompOp	—
`indexFunctor` 📖	CompOp	3 math math: `NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe`, `isIso_indexCone_lift`, `NobelingProof.spanFunctorIsoIndexFunctor_inv_app`
`isoindexConeLift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_indexCone_lift` 📖	mathematical	`T2Space` `TotallyDisconnectedSpace` `IsCompact` `Pi.topologicalSpace`	`CategoryTheory.IsIso` `Profinite` `CompHausLike.category` `TopCat.carrier` `TopCat.str` `CategoryTheory.Limits.Cone.pt` `Opposite` `Finset` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `Finset.partialOrder` `indexFunctor` `indexCone` `limitCone` `CategoryTheory.Limits.IsLimit.lift` `limitConeIsLimit`	—	`CompHausLike.isIso_of_bijective` `IndexFunctor.eq_of_forall_π_app_eq` `IsClosed.preimage` `ContinuousMap.continuous` `T1Space.t1` `Subtype.t1Space` `instT1SpaceForall` `T2Space.t1Space` `IndexFunctor.map_comp_π_app` `Subtype.prop` `IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed` `directed_of_isDirected_le` `Finset.isDirected_le` `Set.Nonempty.preimage` `Set.singleton_nonempty` `IndexFunctor.surjective_π_app` `IsClosed.isCompact` `isCompact_iff_compactSpace` `Set.mem_iInter`

Profinite.IndexFunctor

Definitions

Name	Category	Theorems
`map` 📖	CompOp	1 math math: `map_comp_π_app`
`obj` 📖	CompOp	4 math math: `Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe`, `surjective_π_app`, `Profinite.NobelingProof.iso_map_bijective`, `map_comp_π_app`
`π_app` 📖	CompOp	2 math math: `surjective_π_app`, `map_comp_π_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_forall_π_app_eq` 📖	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `obj` `Finset` `Finset.instMembership` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `ContinuousMap.instFunLike` `π_app`	—	—	`Finset.mem_singleton`
`map_comp_π_app` 📖	mathematical	—	`Set.Elem` `obj` `DFunLike.coe` `ContinuousMap` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `ContinuousMap.instFunLike` `map` `π_app`	—	—
`surjective_π_app` 📖	mathematical	—	`Set.Elem` `obj` `DFunLike.coe` `ContinuousMap` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `ContinuousMap.instFunLike` `π_app`	—	`Subtype.prop`

---

← Back to Index