Tutte

📁 Source: Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Statistics

Metric	Count
Definitions IsTutteViolator	1
Theorems empty, mono, exists_of_isClique_supp, exists_isTutteViolator, not_isTutteViolator_of_isPerfectMatching, tutte	6
Total	7

SimpleGraph

Definitions

Name	Category	Theorems
IsTutteViolator 📖	MathDef	4 math math: exists_isTutteViolator, not_isTutteViolator_of_isPerfectMatching, tutte, IsTutteViolator.empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isTutteViolator 📖	mathematical	Subgraph.IsPerfectMatching Even Nat.card	IsTutteViolator	—	nonempty_fintype exists_maximal_isMatchingFree IsTutteViolator.mono Subgraph.IsPerfectMatching.exists_of_isClique_supp Fintype.card_eq_nat_card Set.ncard_eq_toFinset_card' Set.toFinset_card Mathlib.Tactic.Push.not_forall_eq not_isClique_iff Reachable.exists_path_of_dist Connected.preconnected ConnectedComponent.connected_toSimpleGraph Walk.exists_adj_adj_not_adj_ne Reachable.one_lt_dist_of_ne_of_not_adj Walk.reachable Adj.symm left_lt_sup edge_le_iff Subtype.val_injective adj_comm deleteUniversalVerts_adj
not_isTutteViolator_of_isPerfectMatching 📖	mathematical	Subgraph.IsPerfectMatching	IsTutteViolator	—	Subtype.val_injective Subgraph.IsMatching.eq_of_adj_right ConnectedComponent.eq_of_common_vertex Nat.card_le_card_of_injective Subtype.finite ConnectedComponent.odd_matches_node_outside
tutte 📖	mathematical	—	Subgraph.IsPerfectMatching IsTutteViolator	—	not_isTutteViolator_of_isPerfectMatching Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq IsTutteViolator.empty exists_isTutteViolator Nat.not_odd_iff_even

SimpleGraph.IsTutteViolator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty 📖	mathematical	Odd Nat.instSemiring Nat.card	SimpleGraph.IsTutteViolator Set Set.instEmptyCollection	—	eq_1 Set.ncard_empty Odd.pos Nat.instCanonicallyOrderedAdd Nat.instNontrivial SimpleGraph.odd_ncard_oddComponents Subtype.finite SimpleGraph.Subgraph.deleteVerts_empty Set.ncard_univ
mono 📖	—	SimpleGraph SimpleGraph.instLE SimpleGraph.IsTutteViolator	—	—	SimpleGraph.ncard_oddComponents_mono Subtype.finite SimpleGraph.Subgraph.deleteVerts_mono'

SimpleGraph.Subgraph.IsPerfectMatching

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_of_isClique_supp 📖	mathematical	Even Nat.card SimpleGraph.IsTutteViolator SimpleGraph.universalVerts SimpleGraph.IsClique Set.Elem SimpleGraph.Subgraph.verts SimpleGraph.deleteUniversalVerts SimpleGraph.Subgraph.coe SimpleGraph.ConnectedComponent.supp	SimpleGraph.Subgraph.IsPerfectMatching	—	nonempty_fintype SimpleGraph.IsClique.even_iff_exists_isMatching SimpleGraph.IsClique.subset SimpleGraph.isClique_universalVerts Set.toFinite Subtype.finite Set.even_ncard_compl_iff SimpleGraph.Subgraph.IsMatching.even_card SimpleGraph.Subgraph.IsMatching.sup SimpleGraph.Subgraph.IsMatching.support_eq_verts SimpleGraph.Subgraph.isSpanning_iff SimpleGraph.Subgraph.verts_sup Set.union_compl_self

---

← Back to Index