Documentation Verification Report

EdgeConnectivity

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

Statistics

Metric	Count
Definitions `IsEdgeConnected`, `IsEdgeReachable`	2
Theorems `connected`, `le_degree`, `of_subsingleton`, `preconnected`, `zero`, `anti`, `le_degree`, `mono`, `of_subsingleton`, `reachable`, `refl`, `rfl`, `trans`, `zero`, `not_mem_edges_of_not_isEdgeReachable_two`, `exists_adj_isEdgeReachable_two`, `isBridge_iff_adj_and_not_isEdgeConnected_two`, `isEdgeConnected_add_one`, `isEdgeConnected_one`, `isEdgeConnected_two`, `isEdgeReachable_add_one`, `isEdgeReachable_comm`, `isEdgeReachable_one`, `isEdgeReachable_two`	24
Total	26

SimpleGraph

Definitions

Name	Category	Theorems
`IsEdgeConnected` 📖	MathDef	5 math math: `isEdgeConnected_two`, `isEdgeConnected_add_one`, `IsEdgeConnected.of_subsingleton`, `isEdgeConnected_one`, `IsEdgeConnected.zero`
`IsEdgeReachable` 📖	MathDef	15 math math: `IsEdgeReachable.trans`, `IsEdgeReachable.mono`, `isEdgeReachable_add_one`, `exists_adj_isEdgeReachable_two`, `IsEdgeReachable.of_subsingleton`, `IsEdgeReachable.refl`, `IsEdgeReachable.zero`, `isEdgeReachable_two`, `isEdgeReachable_one`, `IsEdgeReachable.rfl`, `isEdgeReachable_comm`, `IsEdgeReachable.anti`, `IsEdgeReachable.symm`, `isAcyclic_iff_pairwise_not_isEdgeReachable_two`, `isBridge_iff_adj_and_not_isEdgeConnected_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_adj_isEdgeReachable_two` 📖	mathematical	`IsEdgeReachable`	`Adj` `IsEdgeReachable`	—	`Reachable.exists_isPath` `IsEdgeReachable.reachable` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Walk.adj_snd` `Reachable.trans` `Reachable.symm` `Walk.reachable` `Walk.IsPath.eq_snd_of_mem_edges` `Walk.IsPath.tail` `Sym2.eq_swap` `Walk.IsPath.getVert_eq_start_iff_of_not_nil` `Walk.not_nil_of_ne` `Walk.getVert_tail` `deleteEdges_adj` `Mathlib.Tactic.Contrapose.contrapose₄` `Set.subsingleton_iff_singleton` `Set.encard_le_one_iff_subsingleton` `Order.le_of_lt_succ`
`isBridge_iff_adj_and_not_isEdgeConnected_two` 📖	mathematical	—	`IsBridge` `Adj` `IsEdgeReachable`	—	`isBridge_iff` `Eq.trans_lt` `Set.encard_singleton` `Nat.one_lt_ofNat` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `isEdgeReachable_one` `Adj.reachable` `lt_of_le_of_ne` `ENat.lt_coe_add_one_iff` `Set.encard_eq_one` `deleteEdges_adj`
`isEdgeConnected_add_one` 📖	mathematical	—	`IsEdgeConnected` `deleteEdges` `Sym2` `Set` `Set.instSingletonSet`	—	`isEdgeReachable_add_one`
`isEdgeConnected_one` 📖	mathematical	—	`IsEdgeConnected` `Preconnected`	—	—
`isEdgeConnected_two` 📖	mathematical	—	`IsEdgeConnected` `Preconnected` `deleteEdges` `Sym2` `Set` `Set.instSingletonSet`	—	—
`isEdgeReachable_add_one` 📖	mathematical	—	`IsEdgeReachable` `deleteEdges` `Sym2` `Set` `Set.instSingletonSet`	—	`deleteEdges_deleteEdges` `Set.union_comm` `lt_imp_lt_of_le_of_le` `Set.encard_union_le` `le_refl` `Set.encard_singleton` `ENat.add_lt_add_iff_right` `ENat.one_ne_top` `Set.eq_empty_or_nonempty` `deleteEdges_of_subset_diagSet` `IsEdgeReachable.reachable` `Set.insert_diff_self_of_mem` `Set.insert_eq` `Set.encard_diff_singleton_add_one`
`isEdgeReachable_comm` 📖	mathematical	—	`IsEdgeReachable`	—	`IsEdgeReachable.symm`
`isEdgeReachable_one` 📖	mathematical	—	`IsEdgeReachable` `Reachable`	—	`Nat.cast_one` `deleteEdges_of_subset_diagSet`
`isEdgeReachable_two` 📖	mathematical	—	`IsEdgeReachable` `Reachable` `deleteEdges` `Sym2` `Set` `Set.instSingletonSet`	—	—

SimpleGraph.IsEdgeConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connected` 📖	mathematical	`SimpleGraph.IsEdgeConnected`	`SimpleGraph.Connected`	—	`preconnected`
`le_degree` 📖	mathematical	`SimpleGraph.IsEdgeConnected`	`SimpleGraph.degree`	—	`exists_ne` `SimpleGraph.IsEdgeReachable.le_degree`
`of_subsingleton` 📖	mathematical	—	`SimpleGraph.IsEdgeConnected`	—	`SimpleGraph.IsEdgeReachable.of_subsingleton`
`preconnected` 📖	mathematical	`SimpleGraph.IsEdgeConnected`	`SimpleGraph.Preconnected`	—	`SimpleGraph.IsEdgeReachable.reachable`
`zero` 📖	mathematical	—	`SimpleGraph.IsEdgeConnected`	—	`SimpleGraph.IsEdgeReachable.zero`

SimpleGraph.IsEdgeReachable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	mathematical	`SimpleGraph.IsEdgeReachable`	`SimpleGraph.IsEdgeReachable`	—	`lt_imp_lt_of_le_of_le` `le_refl` `Nat.mono_cast` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`le_degree` 📖	mathematical	`SimpleGraph.IsEdgeReachable`	`SimpleGraph.degree`	—	`SimpleGraph.Reachable.exists_isPath` `SimpleGraph.card_incidenceSet_eq_degree` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `SimpleGraph.Walk.adj_snd`
`mono` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE` `SimpleGraph.IsEdgeReachable`	`SimpleGraph.IsEdgeReachable`	—	`SimpleGraph.Reachable.mono` `SimpleGraph.deleteEdges_mono`
`of_subsingleton` 📖	mathematical	—	`SimpleGraph.IsEdgeReachable`	—	`SimpleGraph.Reachable.of_subsingleton`
`reachable` 📖	mathematical	`SimpleGraph.IsEdgeReachable`	`SimpleGraph.Reachable`	—	`SimpleGraph.isEdgeReachable_one` `anti`
`refl` 📖	mathematical	—	`SimpleGraph.IsEdgeReachable`	—	`SimpleGraph.Reachable.rfl`
`rfl` 📖	mathematical	—	`SimpleGraph.IsEdgeReachable`	—	`refl`
`trans` 📖	mathematical	`SimpleGraph.IsEdgeReachable`	`SimpleGraph.IsEdgeReachable`	—	`SimpleGraph.Reachable.trans`
`zero` 📖	mathematical	—	`SimpleGraph.IsEdgeReachable`	—	`Nat.cast_zero` `instIsEmptyFalse`

SimpleGraph.Walk.IsTrail

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_mem_edges_of_not_isEdgeReachable_two` 📖	mathematical	`SimpleGraph.Walk.IsTrail` `SimpleGraph.IsEdgeReachable`	`SimpleGraph.Walk.support`	—	`SimpleGraph.Reachable.trans` `SimpleGraph.isEdgeReachable_two` `disjoint_edges_takeUntil_dropUntil` `SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges` `SimpleGraph.Walk.edges_reverse`

---

← Back to Index