Documentation Verification Report

ConnectedComponents

📁 Source: Mathlib/CategoryTheory/ConnectedComponents.lean

Statistics

Metric	Count
Definitions `ConnectedComponents`, `Component`, `functorToDiscrete`, `liftFunctor`, `mk`, `objectProperty`, `typeToCatHomEquiv`, `ι`, `Decomposed`, `mapConnectedComponents`, `decomposedEquiv`, `decomposedTo`, `inclusion`, `instInhabitedComponent`, `instInhabitedConnectedComponents`, `ConnectedComponents`	16
Theorems `mapConnectedComponents_mk`, `decomposedEquiv_functor`, `decomposedTo_map`, `decomposedTo_obj`, `inclusion_comp_decomposedTo`, `instEssSurjDecomposedDecomposedTo`, `instFaithfulDecomposedDecomposedTo`, `instFullDecomposedDecomposedTo`, `instIsConnectedComponent`, `instIsEquivalenceDecomposedDecomposedTo`, `instNonemptyComponent`	11
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
`ConnectedComponents` 📖	CompOp	8 math math: `instFaithfulDecomposedDecomposedTo`, `instFullDecomposedDecomposedTo`, `decomposedEquiv_functor`, `decomposedTo_map`, `instEssSurjDecomposedDecomposedTo`, `instIsEquivalenceDecomposedDecomposedTo`, `inclusion_comp_decomposedTo`, `decomposedTo_obj`
`Decomposed` 📖	CompOp	8 math math: `instFaithfulDecomposedDecomposedTo`, `instFullDecomposedDecomposedTo`, `decomposedEquiv_functor`, `decomposedTo_map`, `instEssSurjDecomposedDecomposedTo`, `instIsEquivalenceDecomposedDecomposedTo`, `inclusion_comp_decomposedTo`, `decomposedTo_obj`
`decomposedEquiv` 📖	CompOp	1 math math: `decomposedEquiv_functor`
`decomposedTo` 📖	CompOp	8 math math: `instFaithfulDecomposedDecomposedTo`, `instFullDecomposedDecomposedTo`, `decomposedEquiv_functor`, `decomposedTo_map`, `instEssSurjDecomposedDecomposedTo`, `instIsEquivalenceDecomposedDecomposedTo`, `inclusion_comp_decomposedTo`, `decomposedTo_obj`
`inclusion` 📖	CompOp	1 math math: `inclusion_comp_decomposedTo`
`instInhabitedComponent` 📖	CompOp	—
`instInhabitedConnectedComponents` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposedEquiv_functor` 📖	mathematical	—	`Equivalence.functor` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedEquiv` `decomposedTo`	—	—
`decomposedTo_map` 📖	mathematical	—	`Functor.map` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo` `Sigma.descMap` `ConnectedComponents.ι`	—	—
`decomposedTo_obj` 📖	mathematical	—	`Functor.obj` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo` `ObjectProperty.FullSubcategory.obj`	—	—
`inclusion_comp_decomposedTo` 📖	mathematical	—	`Functor.comp` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `Decomposed` `Sigma.sigma` `ConnectedComponents` `inclusion` `decomposedTo` `ConnectedComponents.ι`	—	—
`instEssSurjDecomposedDecomposedTo` 📖	mathematical	—	`Functor.EssSurj` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo`	—	—
`instFaithfulDecomposedDecomposedTo` 📖	mathematical	—	`Functor.Faithful` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo`	—	—
`instFullDecomposedDecomposedTo` 📖	mathematical	—	`Functor.Full` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo`	—	`Quotient.eq''` `Relation.ReflTransGen.single`
`instIsConnectedComponent` 📖	mathematical	—	`IsConnected` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty`	—	`isConnected_of_zigzag` `instNonemptyComponent` `Quotient.exact'` `List.exists_isChain_cons_of_relationReflTransGen` `Quotient.sound'` `List.IsChain.backwards_cons_induction` `Relation.ReflTransGen.head` `List.isChain_cons_pmap_of_isChain_cons` `zag_of_zag_obj` `ObjectProperty.full_ι`
`instIsEquivalenceDecomposedDecomposedTo` 📖	mathematical	—	`Functor.IsEquivalence` `Decomposed` `Sigma.sigma` `ConnectedComponents` `ConnectedComponents.Component` `ObjectProperty.FullSubcategory.category` `ConnectedComponents.objectProperty` `decomposedTo`	—	`instFaithfulDecomposedDecomposedTo` `instFullDecomposedDecomposedTo` `instEssSurjDecomposedDecomposedTo`
`instNonemptyComponent` 📖	mathematical	—	`ConnectedComponents.Component`	—	`Quotient.inductionOn'`

CategoryTheory.ConnectedComponents

Definitions

Name	Category	Theorems
`Component` 📖	CompOp	10 math math: `CategoryTheory.instFaithfulDecomposedDecomposedTo`, `CategoryTheory.instFullDecomposedDecomposedTo`, `CategoryTheory.decomposedEquiv_functor`, `CategoryTheory.decomposedTo_map`, `CategoryTheory.instEssSurjDecomposedDecomposedTo`, `CategoryTheory.instIsEquivalenceDecomposedDecomposedTo`, `CategoryTheory.instIsConnectedComponent`, `CategoryTheory.inclusion_comp_decomposedTo`, `CategoryTheory.decomposedTo_obj`, `CategoryTheory.instNonemptyComponent`
`functorToDiscrete` 📖	CompOp	—
`liftFunctor` 📖	CompOp	—
`mk` 📖	CompOp	—
`objectProperty` 📖	CompOp	9 math math: `CategoryTheory.instFaithfulDecomposedDecomposedTo`, `CategoryTheory.instFullDecomposedDecomposedTo`, `CategoryTheory.decomposedEquiv_functor`, `CategoryTheory.decomposedTo_map`, `CategoryTheory.instEssSurjDecomposedDecomposedTo`, `CategoryTheory.instIsEquivalenceDecomposedDecomposedTo`, `CategoryTheory.instIsConnectedComponent`, `CategoryTheory.inclusion_comp_decomposedTo`, `CategoryTheory.decomposedTo_obj`
`typeToCatHomEquiv` 📖	CompOp	—
`ι` 📖	CompOp	2 math math: `CategoryTheory.decomposedTo_map`, `CategoryTheory.inclusion_comp_decomposedTo`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapConnectedComponents` 📖	CompOp	1 math math: `mapConnectedComponents_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapConnectedComponents_mk` 📖	mathematical	—	`mapConnectedComponents` `CategoryTheory.Zigzag.setoid` `obj`	—	—

(root)

Definitions

Name	Category	Theorems
`ConnectedComponents` 📖	CompOp	15 math math: `connectedComponents_preimage_singleton`, `connectedComponents_preimage_image`, `ConnectedComponents.surjective_coe`, `instCompactSpaceConnectedComponents`, `CompHaus.toProfinite_obj'`, `Continuous.connectedComponentsLift_comp_coe`, `ConnectedComponents.continuous_coe`, `Continuous.connectedComponentsMap_continuous`, `ConnectedComponents.t2`, `ConnectedComponents.isQuotientMap_coe`, `Continuous.connectedComponentsLift_continuous`, `instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace`, `instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace`, `ConnectedComponents.range_coe`, `ConnectedComponents.totallyDisconnectedSpace`

---

← Back to Index