Documentation Verification Report

Finite

📁 Source: Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean

Statistics

Metric	Count
Definitions `instDecidableConnected`, `instDecidableMemSupp`, `instDecidablePreconnected`, `instDecidableRelReachable`, `instFintypeConnectedComponent`, `oddComponents`	6
Theorems `card_le_card_of_le`, `odd_oddComponents_ncard_subset_supp`, `disjiUnion_supp_toFinset_eq_supp_toFinset`, `ncard_oddComponents_mono`, `odd_ncard_oddComponents`, `reachable_iff_exists_finsetWalkLength_nonempty`	6
Total	12

SimpleGraph

Definitions

Name	Category	Theorems
`instDecidableConnected` 📖	CompOp	—
`instDecidableMemSupp` 📖	CompOp	2 math math: `disjiUnion_supp_toFinset_eq_supp_toFinset`, `ConnectedComponent.even_card_of_isPerfectMatching`
`instDecidablePreconnected` 📖	CompOp	—
`instDecidableRelReachable` 📖	CompOp	—
`instFintypeConnectedComponent` 📖	CompOp	2 math math: `card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix`, `disjiUnion_supp_toFinset_eq_supp_toFinset`
`oddComponents` 📖	CompOp	4 math math: `ncard_oddComponents_mono`, `ConnectedComponent.odd_matches_node_outside`, `odd_ncard_oddComponents`, `ConnectedComponent.odd_oddComponents_ncard_subset_supp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjiUnion_supp_toFinset_eq_supp_toFinset` 📖	mathematical	`SimpleGraph` `instLE`	`Finset.disjiUnion` `ConnectedComponent` `Finset.filter` `Set` `Set.instHasSubset` `ConnectedComponent.supp` `Finset.univ` `instFintypeConnectedComponent` `Set.toFinset` `Subtype.fintype` `Set.instMembership` `instDecidableMemSupp`	—	`Finset.coe_injective` `Finset.disjiUnion_eq_biUnion` `Finset.coe_biUnion` `Set.iUnion_congr_Prop` `Finset.coe_filter` `Set.coe_toFinset` `ConnectedComponent.biUnion_supp_eq_supp`
`ncard_oddComponents_mono` 📖	mathematical	`SimpleGraph` `instLE`	`Set.ncard` `ConnectedComponent` `oddComponents`	—	`Set.nonempty_of_ncard_ne_zero` `ConnectedComponent.odd_oddComponents_ncard_subset_supp` `Nat.card_le_card_of_injective` `Subtype.finite` `ConnectedComponent.instFinite` `Subtype.val_injective` `ConnectedComponent.eq_of_common_vertex` `ConnectedComponent.nonempty_supp` `Set.Nonempty.some_mem`
`odd_ncard_oddComponents` 📖	mathematical	—	`Odd` `Nat.instSemiring` `Set.ncard` `ConnectedComponent` `oddComponents` `Nat.card`	—	`nonempty_fintype` `Nat.card_eq_fintype_card` `set_fintype_card_eq_univ_iff` `iUnion_connectedComponentSupp` `Set.toFinset_iUnion` `Finset.card_biUnion` `Set.disjoint_toFinset` `pairwise_disjoint_supp_connectedComponent` `Finset.sum_congr` `Set.ncard_coe_finset` `Finset.odd_sum_iff_odd_card_odd`
`reachable_iff_exists_finsetWalkLength_nonempty` 📖	mathematical	—	`Reachable` `Fintype.card` `Finset.Nonempty` `Walk` `finsetWalkLength` `neighborSetFintype`	—	`Reachable.elim_path` `Walk.IsPath.length_lt` `Path.isPath`

SimpleGraph.ConnectedComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_of_le` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`Nat.card` `SimpleGraph.ConnectedComponent`	—	`Nat.card_le_card_of_surjective` `instFinite` `surjective_map_ofLE`
`odd_oddComponents_ncard_subset_supp` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`Odd` `Nat.instSemiring` `Set.ncard` `SimpleGraph.ConnectedComponent` `setOf` `Set` `Set.instMembership` `SimpleGraph.oddComponents` `Set.instHasSubset` `supp`	—	`nonempty_fintype` `Nat.card_eq_card_toFinset` `SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset` `Finset.card_disjiUnion` `Finset.sum_congr` `Set.toFinset_card` `Fintype.card_ofFinset` `Finset.odd_sum_iff_odd_card_odd` `Nat.card_eq_fintype_card` `Finset.ext` `Finset.filter.congr_simp` `Set.toFinset_setOf` `Finset.coe_filter`

---

← Back to Index