Theorems · Theorem · combinatorics
SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq
∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V),
{x ∈ s | x ∈ p.support}.Nonempty → ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x- Cited by
- 0 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- SimpleGraphstatement and proof · cited by 3,072
- Finset.Nonemptystatement and proof · cited by 1,001
- Finset.filterstatement and proof · cited by 949
- SimpleGraph.Walkstatement and proof · cited by 915
- Finset.eraseproof · cited by 455
- SimpleGraph.Walk.supportstatement and proof · cited by 307
- SimpleGraph.Walk.takeUntilstatement and proof · cited by 58
- Finset.subset_insert_iffproof · cited by 11
- Finset.subset_emptyproof · cited by 4
- Finset.filter_eraseproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.