Documentation Verification Report

ConnectedComponent

📁 Source: Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

Statistics

Metric	Count
Definitions `IsSStronglyConnected`, `IsStronglyConnected`, `StronglyConnectedComponent`, `instCoe`, `instInhabited`, `mk`, `WeaklyConnectedComponent`, `instCoeTC`, `instInhabited`, `mk`, `stronglyConnectedSetoid`, `wideSubquiverSymmetrify`, `zigzagSetoid`, `ConnectedComponent`	14
Theorems `exists_pos_cycle`, `exists_pos_path`, `isStronglyConnected`, `isSStronglyConnected_of_hom`, `isStronglyConnected_symmetrify`, `nonempty_path`, `pos_cycle`, `eq`, `mk_eq_mk`, `eq`, `exists_path_of_stronglyConnectedComponent_eq`, `isSStronglyConnected_iff`, `isStronglyConnected_iff`, `stronglyConnectedComponent_eq_of_path`, `stronglyConnectedComponent_singleton_iff`	15
Total	29

Quiver

Definitions

Name	Category	Theorems
`IsSStronglyConnected` 📖	MathDef	4 math math: `IsStronglyConnected.isSStronglyConnected_of_hom`, `Matrix.isIrreducible_iff`, `Matrix.IsIrreducible.connected`, `isSStronglyConnected_iff`
`IsStronglyConnected` 📖	MathDef	2 math math: `isStronglyConnected_iff`, `IsSStronglyConnected.isStronglyConnected`
`StronglyConnectedComponent` 📖	CompOp	—
`WeaklyConnectedComponent` 📖	CompOp	—
`stronglyConnectedSetoid` 📖	CompOp	—
`wideSubquiverSymmetrify` 📖	CompOp	—
`zigzagSetoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_path_of_stronglyConnectedComponent_eq` 📖	mathematical	—	`Path`	—	`StronglyConnectedComponent.eq`
`isSStronglyConnected_iff` 📖	mathematical	—	`IsSStronglyConnected` `Path.length`	—	—
`isStronglyConnected_iff` 📖	mathematical	—	`IsStronglyConnected` `Path`	—	—
`stronglyConnectedComponent_eq_of_path` 📖	—	—	—	—	`StronglyConnectedComponent.eq`
`stronglyConnectedComponent_singleton_iff` 📖	mathematical	—	`Path`	—	`stronglyConnectedComponent_eq_of_path` `exists_path_of_stronglyConnectedComponent_eq`

Quiver.IsSStronglyConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos_cycle` 📖	mathematical	`Quiver.IsSStronglyConnected`	`Quiver.Path.length`	—	—
`exists_pos_path` 📖	mathematical	`Quiver.IsSStronglyConnected`	`Quiver.Path.length`	—	—
`isStronglyConnected` 📖	mathematical	`Quiver.IsSStronglyConnected`	`Quiver.IsStronglyConnected`	—	—

Quiver.IsStronglyConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSStronglyConnected_of_hom` 📖	mathematical	`Quiver.IsStronglyConnected`	`Quiver.IsSStronglyConnected`	—	`Quiver.Path.length_comp`
`isStronglyConnected_symmetrify` 📖	mathematical	`Quiver.IsStronglyConnected`	`Quiver.Symmetrify` `Quiver.symmetrifyQuiver`	—	—
`nonempty_path` 📖	mathematical	`Quiver.IsStronglyConnected`	`Quiver.Path`	—	—

Quiver.StronglyConnectedComponent

Definitions

Name	Category	Theorems
`instCoe` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`Quiver.Path`	—	`Quotient.eq''`
`mk_eq_mk` 📖	mathematical	—	`Quiver.Path`	—	`eq`

Quiver.StronglyConnectedComponent.IsSStronglyConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pos_cycle` 📖	mathematical	`Quiver.IsSStronglyConnected`	`Quiver.Path.length`	—	—

Quiver.WeaklyConnectedComponent

Definitions

Name	Category	Theorems
`instCoeTC` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`Quiver.Path` `Quiver.Symmetrify` `Quiver.symmetrifyQuiver`	—	`Quotient.eq''`

SimpleGraph

Definitions

Name	Category	Theorems
`ConnectedComponent` 📖	CompOp	36 math math: `colorable_iff_forall_connectedComponents`, `ConnectedComponent.supp_injective`, `iUnion_connectedComponentSupp`, `ConnectedComponent.instNonempty`, `homOfConnectedComponents_apply`, `Iso.connectedComponentEquiv_symm_apply`, `ConnectedComponent.instSubsingleton`, `card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix`, `disjiUnion_supp_toFinset_eq_supp_toFinset`, `ncard_oddComponents_mono`, `ConnectedComponent.card_le_card_of_le`, `Preconnected.subsingleton_connectedComponent`, `IsCycles.toSimpleGraph`, `ConnectedComponent.odd_matches_node_outside`, `linearIndependent_lapMatrix_ker_basis_aux`, `ConnectedComponent.instFinite`, `top_le_span_range_lapMatrix_ker_basis_aux`, `ConnectedComponent.adj_spanningCoe_toSimpleGraph`, `ConnectedComponent.isEmpty`, `Iso.connectedComponentEquiv_refl`, `ConnectedComponent.connectedComponentMk_mem`, `ConnectedComponent.toSimpleGraph_hom_apply`, `ConnectedComponent.spanningCoe_toSubgraph`, `pairwise_disjoint_supp_connectedComponent`, `ConnectedComponent.Represents.ncard_eq`, `ConnectedComponent.surjective_map_ofLE`, `ConnectedComponent.connected_toSimpleGraph`, `Iso.connectedComponentEquiv_trans`, `IsAcyclic.isTree_connectedComponent`, `odd_ncard_oddComponents`, `ConnectedComponent.inhabited_default`, `Iso.connectedComponentEquiv_apply`, `ConnectedComponent.odd_oddComponents_ncard_subset_supp`, `ConnectedComponent.biUnion_supp_eq_supp`, `Iso.connectedComponentEquiv_symm`, `mem_ker_toLin'_lapMatrix_of_connectedComponent`

---

← Back to Index