EdgeConnectivity

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

Statistics

Metric	Count
Definitions IsEdgeConnected, IsEdgeReachable	2
Theorems connected, preconnected, zero, anti, mono, reachable, refl, rfl, trans, zero, not_mem_edges_of_not_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	19
Total	21

SimpleGraph

Definitions

Name	Category	Theorems
IsEdgeConnected 📖	MathDef	4 math math: isEdgeConnected_two, isEdgeConnected_add_one, isEdgeConnected_one, IsEdgeConnected.zero
IsEdgeReachable 📖	MathDef	8 math math: isEdgeReachable_add_one, IsEdgeReachable.refl, IsEdgeReachable.zero, isEdgeReachable_two, isEdgeReachable_one, IsEdgeReachable.rfl, isEdgeReachable_comm, isBridge_iff_adj_and_not_isEdgeConnected_two

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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 IsOrderedRing.toZeroLEOneClass 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 forall_swap
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
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 📖	—	SimpleGraph.IsEdgeReachable	—	—	lt_imp_lt_of_le_of_le le_refl Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
mono 📖	—	SimpleGraph SimpleGraph.instLE SimpleGraph.IsEdgeReachable	—	—	SimpleGraph.Reachable.mono SimpleGraph.deleteEdges_mono
reachable 📖	mathematical	SimpleGraph.IsEdgeReachable	SimpleGraph.Reachable	—	SimpleGraph.isEdgeReachable_one anti
refl 📖	mathematical	—	SimpleGraph.IsEdgeReachable	—	SimpleGraph.Reachable.rfl
rfl 📖	mathematical	—	SimpleGraph.IsEdgeReachable	—	refl
trans 📖	—	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