Loogle!

Result

Found 917 declarations mentioning SimpleGraph.Walk. Of these, only the first 200 are shown.

• SimpleGraph.Walk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} (G : SimpleGraph V) : V → V → Type u
• SimpleGraph.Walk.nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u : V} : G.Walk u u
• SimpleGraph.Walk.nil' 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (u : V) : G.Walk u u
• SimpleGraph.Walk.instInhabited 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} (G : SimpleGraph V) (v : V) : Inhabited (G.Walk v v)
• SimpleGraph.Walk.Nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} : G.Walk v w → Prop
• SimpleGraph.Walk.length 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → ℕ
• SimpleGraph.Walk.support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → List V
• SimpleGraph.instDecidableEqWalk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V✝ : Type u_1} {G✝ : SimpleGraph V✝} {a✝ a✝¹ : V✝} [DecidableEq V✝] : DecidableEq (G✝.Walk a✝ a✝¹)
• SimpleGraph.Walk.edgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set (Sym2 V)
• SimpleGraph.Walk.edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List (Sym2 V)
• SimpleGraph.Walk.darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → List G.Dart
• SimpleGraph.Adj.toWalk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : G.Walk u v
• SimpleGraph.Walk.instDecidableNil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) : Decidable p.Nil
• SimpleGraph.Walk.nil_of_subsingleton 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} [Subsingleton V] (p : G.Walk v w) : p.Nil
• SimpleGraph.Walk.edges_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.edges
• SimpleGraph.Walk.darts_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.darts
• SimpleGraph.Walk.Nil.eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil → v = w
• SimpleGraph.Walk.cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : G.Walk u w
• SimpleGraph.Walk.cons' 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (u v w : V) (h : G.Adj u v) (p : G.Walk v w) : G.Walk u w
• SimpleGraph.Walk.isChain_adj_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.Adj p.support
• SimpleGraph.Walk.not_nil_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : v ≠ w → ¬p.Nil
• SimpleGraph.Walk.support_ne_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support ≠ []
• SimpleGraph.Walk.end_mem_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : v ∈ p.support
• SimpleGraph.Walk.isChain_dartAdj_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.IsChain G.DartAdj p.darts
• SimpleGraph.Walk.start_mem_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u ∈ p.support
• SimpleGraph.Walk.default_def 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} (G : SimpleGraph V) (v : V) : default = SimpleGraph.Walk.nil
• SimpleGraph.instDecidableEqWalk.decEq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V✝ : Type u_1} {G✝ : SimpleGraph V✝} {a✝ a✝¹ : V✝} [DecidableEq V✝] (x✝ x✝¹ : G✝.Walk a✝ a✝¹) : Decidable (x✝ = x✝¹)
• SimpleGraph.Walk.Nil.eq_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil → p = SimpleGraph.Walk.nil
• SimpleGraph.Walk.eq_nil_iff_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p = SimpleGraph.Walk.nil ↔ p.Nil
• SimpleGraph.Walk.eq_of_length_eq_zero 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 0 → u = v
• SimpleGraph.Walk.exists_nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ p, p.Nil) ↔ u = v
• SimpleGraph.Walk.getLast_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.getLast ⋯ = b
• SimpleGraph.Walk.head_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.head ⋯ = a
• SimpleGraph.Walk.length_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.edges.length = p.length
• SimpleGraph.Walk.nil_iff_eq_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil ↔ p = SimpleGraph.Walk.nil
• SimpleGraph.Walk.adj_of_length_eq_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 1 → G.Adj u v
• SimpleGraph.Walk.darts_nodup_of_support_nodup 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.darts.Nodup
• SimpleGraph.Walk.length_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.darts.length = p.length
• SimpleGraph.Walk.ofSupport 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (l : List V) (hne : l ≠ []) (hchain : List.IsChain G.Adj l) : G.Walk (l.head hne) (l.getLast hne)
• SimpleGraph.Walk.support_nonempty 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : {w | w ∈ p.support}.Nonempty
• SimpleGraph.Walk.end_mem_tail_support_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : u ≠ v) (p : G.Walk u v) : v ∈ p.support.tail
• SimpleGraph.Walk.Nil.length_eq_zero 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.Nil → p.length = 0
• SimpleGraph.Walk.cons_tail_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u :: p.support.tail = p.support
• SimpleGraph.Walk.edges_eq_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.edges = [] ↔ p.Nil
• SimpleGraph.Walk.isChain_adj_cons_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : List.IsChain G.Adj (u :: p.support)
• SimpleGraph.Walk.length_eq_zero_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 0 ↔ p.Nil
• SimpleGraph.Walk.nil_iff_length_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil ↔ p.length = 0
• SimpleGraph.Walk.not_nil_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : ¬(SimpleGraph.Walk.cons h p).Nil
• SimpleGraph.Walk.support_eq_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support = u :: p.support.tail
• SimpleGraph.Walk.nil_iff_support_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil ↔ p.support = [v]
• SimpleGraph.Walk.darts_eq_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.darts = [] ↔ p.Nil
• SimpleGraph.Walk.end_mem_tail_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : v ∈ p.support.tail
• SimpleGraph.Walk.not_nil_iff_lt_length 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ 0 < p.length
• SimpleGraph.Walk.edgeSet_eq_empty 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.edgeSet = ∅ ↔ p.Nil
• SimpleGraph.Walk.exists_length_eq_zero_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ p, p.length = 0) ↔ u = v
• SimpleGraph.Walk.nil_of_isIsolated_of_mem_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hw : G.IsIsolated w) (hwp : w ∈ p.support) : p.Nil
• SimpleGraph.Walk.edges_eq_map_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.edges = List.map SimpleGraph.Dart.edge p.darts
• SimpleGraph.Walk.exists_length_eq_one_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ p, p.length = 1) ↔ G.Adj u v
• SimpleGraph.Walk.adj_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v x y : V} (p : G.Walk u v) (h : s(x, y) ∈ p.edges) : G.Adj x y
• SimpleGraph.Walk.support_suffix_support_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk v w) (hadj : G.Adj u v) : p.support <:+ (SimpleGraph.Walk.cons hadj p).support
• SimpleGraph.Walk.length_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1
• SimpleGraph.Walk.support_subset_support_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk v w) (hadj : G.Adj u v) : p.support ⊆ (SimpleGraph.Walk.cons hadj p).support
• SimpleGraph.Walk.edges_subset_edgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄ : e ∈ p.edges → e ∈ G.edgeSet
• SimpleGraph.Walk.isChain_dartAdj_cons_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v w : V} (h : d.toProd.2 = v) (p : G.Walk v w) : List.IsChain G.DartAdj (d :: p.darts)
• SimpleGraph.Walk.support_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).support = u :: p.support
• SimpleGraph.Walk.map_fst_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun x => x.toProd.1) p.darts = p.support.dropLast
• SimpleGraph.Walk.map_snd_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun x => x.toProd.2) p.darts = p.support.tail
• SimpleGraph.Walk.cons_map_snd_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u :: List.map (fun x => x.toProd.2) p.darts = p.support
• SimpleGraph.Walk.edges_eq_zipWith_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.edges = List.zipWith (fun x1 x2 => s(x1, x2)) p.support p.support.tail
• SimpleGraph.Walk.mem_edgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {e : Sym2 V} : e ∈ p.edgeSet ↔ e ∈ p.edges
• SimpleGraph.Walk.mem_support_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) : w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
• SimpleGraph.Walk.edges_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges
• SimpleGraph.Walk.support_getElem_zero 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support[0] = u
• SimpleGraph.Walk.support_getElem_length 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support[p.length] = v
• SimpleGraph.Walk.coe_edges_toFinset 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : ↑p.edges.toFinset = p.edgeSet
• SimpleGraph.Walk.length_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).length = p.length + 1
• SimpleGraph.Walk.coe_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : ↑p.support = {u} + ↑p.support.tail
• SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart} : d ∈ p.darts → d.toProd.1 ∈ p.support
• SimpleGraph.Walk.eq_of_length_le_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (hp : p.length ≤ 1) (hq : q.length ≤ 1) : p = q
• SimpleGraph.Walk.edgeSet_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).edgeSet = insert s(u, v) p.edgeSet
• SimpleGraph.Walk.ofDarts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (l : List G.Dart) (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l) : G.Walk (l.head hne).toProd.1 (l.getLast hne).toProd.2
• SimpleGraph.Walk.darts_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).darts = { fst := u, snd := v, adj := h } :: p.darts
• SimpleGraph.Walk.exists_eq_cons_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (hne : u ≠ v) (p : G.Walk u v) : ∃ w, ∃ (h : G.Adj u w), ∃ p', p = SimpleGraph.Walk.cons h p'
• SimpleGraph.Walk.ofSupport_singleton 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} (G : SimpleGraph V) (v : V) : SimpleGraph.Walk.ofSupport [v] ⋯ ⋯ = SimpleGraph.Walk.nil
• SimpleGraph.Walk.map_fst_darts_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.map (fun x => x.toProd.1) p.darts ++ [v] = p.support
• SimpleGraph.Walk.not_nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, p = SimpleGraph.Walk.cons h q
• SimpleGraph.Walk.mem_darts_iff_fst_snd_infix_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {d : G.Dart} : d ∈ p.darts ↔ [d.toProd.1, d.toProd.2] <:+: p.support
• SimpleGraph.Walk.mem_darts_iff_infix_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : G.Adj u' v') : { fst := u', snd := v', adj := h } ∈ p.darts ↔ [u', v'] <:+: p.support
• SimpleGraph.Walk.mem_support_iff_exists_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} : w ∈ p.support ↔ w = v ∨ ∃ e ∈ p.edges, w ∈ e
• SimpleGraph.Walk.mem_support_iff_exists_mem_edges_of_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hnil : ¬p.Nil) : w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e
• SimpleGraph.Walk.notNilRec 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (p : G.Walk u w) (hp : ¬p.Nil) : motive p hp
• SimpleGraph.Walk.exists_boundary_dart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) : ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
• SimpleGraph.Walk.ofDarts_singleton' 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (d : G.Dart) : SimpleGraph.Walk.ofDarts [d] ⋯ ⋯ = ⋯.toWalk
• SimpleGraph.Walk.fst_darts_getElem 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (hi : i < p.darts.length) : p.darts[i].toProd.1 = p.support.dropLast[i]
• SimpleGraph.Walk.getElem_edges_eq_edge_getElem_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length) : p.edges[i] = p.darts[i].edge
• SimpleGraph.Walk.snd_darts_getElem 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (hi : i < p.darts.length) : p.darts[i].toProd.2 = p.support.tail[i]
• SimpleGraph.Walk.edge_getElem_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.darts.length) : p.darts[i].edge = p.edges[i]
• SimpleGraph.Walk.notNilRec_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (h' : G.Adj u v) (q' : G.Walk v w) : SimpleGraph.Walk.notNilRec (fun {u v w} => cons) (SimpleGraph.Walk.cons h' q') ⋯ = cons h' q'
• SimpleGraph.Walk.ofSupport_cons_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} {l : List V} (hchain : List.IsChain G.Adj (u :: v :: l)) : SimpleGraph.Walk.ofSupport (u :: v :: l) ⋯ hchain = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.ofSupport (v :: l) ⋯ ⋯)
• SimpleGraph.Walk.ofDarts_singleton 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} (d : G.Dart) : SimpleGraph.Walk.ofDarts [d] ⋯ ⋯ = SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil
• SimpleGraph.Walk.ofDarts_cons_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {d₁ d₂ : G.Dart} {l : List G.Dart} (hchain : List.IsChain G.DartAdj (d₁ :: d₂ :: l)) : SimpleGraph.Walk.ofDarts (d₁ :: d₂ :: l) ⋯ hchain = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.ofDarts (d₂ :: l) ⋯ ⋯)
• SimpleGraph.Walk.penultimate 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : V
• SimpleGraph.Walk.snd 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : V
• SimpleGraph.Walk.getVert 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → ℕ → V
• SimpleGraph.Walk.firstDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : G.Dart
• SimpleGraph.Walk.lastDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : G.Dart
• SimpleGraph.Walk.getVert_zero 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : w.getVert 0 = u
• SimpleGraph.Walk.getVert_length 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : w.getVert w.length = v
• SimpleGraph.Walk.adj_penultimate 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj p.penultimate w
• SimpleGraph.Walk.adj_snd 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj v p.snd
• SimpleGraph.Walk.getVert_eq_getD_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : p.getVert n = p.support.getD n v
• SimpleGraph.Walk.getVert_mem_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (i : ℕ) : p.getVert i ∈ p.support
• SimpleGraph.Walk.getVert_of_length_le 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ} (hi : w.length ≤ i) : w.getVert i = v
• SimpleGraph.Walk.snd_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w : V} (q : G.Walk v w) (hadj : G.Adj u v) : (SimpleGraph.Walk.cons hadj q).snd = v
• SimpleGraph.Walk.adj_of_infix_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : [u', v'] <:+: p.support) : G.Adj u' v'
• SimpleGraph.Walk.penultimate_mem_dropLast_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.penultimate ∈ p.support.dropLast
• SimpleGraph.Walk.snd_mem_tail_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.snd ∈ p.support.tail
• SimpleGraph.Walk.edge_firstDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).edge = s(v, p.snd)
• SimpleGraph.Walk.edge_lastDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.lastDart hp).edge = s(p.penultimate, w)
• SimpleGraph.Walk.firstDart_toProd 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).toProd = (v, p.snd)
• SimpleGraph.Walk.lastDart_toProd 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.lastDart hp).toProd = (p.penultimate, w)
• SimpleGraph.Walk.mk_penultimate_end_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(p.penultimate, w) ∈ p.edges
• SimpleGraph.Walk.mk_start_snd_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(v, p.snd) ∈ p.edges
• SimpleGraph.Walk.range_getVert_eq_range_support_getElem 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set.range p.getVert = Set.range p.support.get
• SimpleGraph.Walk.firstDart_mem_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.firstDart hnil ∈ p.darts
• SimpleGraph.Walk.lastDart_mem_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.lastDart hnil ∈ p.darts
• SimpleGraph.Walk.penultimate_cons_of_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ¬p.Nil) : (SimpleGraph.Walk.cons h p).penultimate = p.penultimate
• SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []) : p.edges.getLast hp = s(p.penultimate, w)
• SimpleGraph.Walk.head_edges_eq_mk_start_snd 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []) : p.edges.head hp = s(v, p.snd)
• SimpleGraph.Walk.getVert_support_idxOf 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support) : p.getVert (List.idxOf w p.support) = w
• SimpleGraph.Walk.adj_getVert_succ 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) : G.Adj (w.getVert i) (w.getVert (i + 1))
• SimpleGraph.Walk.getVert_cons_succ 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v) : (SimpleGraph.Walk.cons h p).getVert (n + 1) = p.getVert n
• SimpleGraph.Walk.getVert_comp_val_eq_get_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.getVert ∘ Fin.val = p.support.get
• SimpleGraph.Walk.getVert_eq_support_getElem? 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length) : some (p.getVert n) = p.support[n]?
• SimpleGraph.Walk.penultimate_cons_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w w' : V} (h : G.Adj u v) (h₂ : G.Adj v w) (p : G.Walk w w') : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h₂ p)).penultimate = (SimpleGraph.Walk.cons h₂ p).penultimate
• SimpleGraph.Walk.support_getElem_eq_getVert 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n < p.support.length) : p.support[n] = p.getVert n
• SimpleGraph.Walk.getVert_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) : (SimpleGraph.Walk.cons h p).getVert n = p.getVert (n - 1)
• SimpleGraph.Walk.snd_eq_support_getElem_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hnil : ¬p.Nil) : p.snd = p.support[1]
• SimpleGraph.Walk.support_getElem_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : 1 < p.support.length) : p.support[1] = p.snd
• SimpleGraph.Walk.support_getElem_length_sub_one_eq_penultimate 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.support[p.length - 1] = p.penultimate
• SimpleGraph.Walk.mk_mem_edges_iff_exists 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) : s(u', v') ∈ p.edges ↔ ∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')
• SimpleGraph.Walk.firstDart_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length) : p.firstDart h₁ = p.darts[0]
• SimpleGraph.Walk.getElem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length) : p.edges[i] = s(p.getVert i, p.getVert (i + 1))
• SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(p.penultimate, w) = p.edges.getLast ⋯
• SimpleGraph.Walk.mk_start_snd_eq_head_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(v, p.snd) = p.edges.head ⋯
• SimpleGraph.Walk.firstDart_eq_head_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.firstDart hnil = p.darts.head ⋯
• SimpleGraph.Walk.lastDart_eq_getLast_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.lastDart hnil = p.darts.getLast ⋯
• SimpleGraph.Walk.getLast_darts_eq_lastDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []) : p.darts.getLast hnil = p.lastDart ⋯
• SimpleGraph.Walk.head_darts_eq_firstDart 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []) : p.darts.head hnil = p.firstDart ⋯
• SimpleGraph.Walk.lastDart_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length) : p.lastDart h₁ = p.darts[p.darts.length - 1]
• SimpleGraph.Walk.darts_getElem_eq_getVert 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p.darts.length) : p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }
• SimpleGraph.Walk.getVert_eq_support_getElem 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
  {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length) : p.getVert n = p.support[n]
• SimpleGraph.Walk.reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : G.Walk v u
• SimpleGraph.Walk.support_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.support
• SimpleGraph.Walk.dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.Walk u p.penultimate
• SimpleGraph.Walk.tail 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.Walk p.snd v
• SimpleGraph.Walk.append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} : G.Walk u v → G.Walk v w → G.Walk u w
• SimpleGraph.Walk.concat 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : G.Walk u w
• SimpleGraph.Walk.reverseAux 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} : G.Walk u v → G.Walk u w → G.Walk v w
• SimpleGraph.Walk.reverse_bijective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Bijective SimpleGraph.Walk.reverse
• SimpleGraph.Walk.reverse_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.reverse
• SimpleGraph.Walk.reverse_surjective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Surjective SimpleGraph.Walk.reverse
• SimpleGraph.Walk.drop 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk (p.getVert n) v
• SimpleGraph.Walk.take 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk u (p.getVert n)
• SimpleGraph.Walk.reverse_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil
• SimpleGraph.Walk.copy 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : G.Walk u' v'
• SimpleGraph.Walk.edges_nodup_of_support_nodup 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.edges.Nodup
• SimpleGraph.Walk.tail_support_perm_dropLast_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.support.tail.Perm p.support.dropLast
• SimpleGraph.Walk.append_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.append SimpleGraph.Walk.nil = p
• SimpleGraph.Walk.nil_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : SimpleGraph.Walk.nil.append p = p
• SimpleGraph.Walk.nil_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.reverse.Nil ↔ p.Nil
• SimpleGraph.Walk.reverse_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.reverse = p
• SimpleGraph.Walk.length_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.length = p.length
• SimpleGraph.Walk.penultimate_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.penultimate = p.snd
• SimpleGraph.Walk.snd_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.snd = p.penultimate
• SimpleGraph.Walk.support_eq_concat 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support = p.support.dropLast.concat v
• SimpleGraph.Walk.copy_rfl_rfl 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.copy ⋯ ⋯ = p
• SimpleGraph.Walk.dropLast_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v : V} : SimpleGraph.Walk.nil.dropLast = SimpleGraph.Walk.nil
• SimpleGraph.Walk.edgeSet_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.edgeSet = p.edgeSet
• SimpleGraph.Walk.copy_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u u' : V} (hu : u = u') : SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil
• SimpleGraph.Walk.penultimate_concat 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj v t) : (p.concat h).penultimate = v
• SimpleGraph.Walk.support_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.support = p.support.reverse
• SimpleGraph.Walk.Nil.dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.Nil) : p.dropLast.Nil
• SimpleGraph.Walk.Nil.tail 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.Nil) : p.tail.Nil
• SimpleGraph.Walk.concat_ne_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (h : G.Adj v u) : p.concat h ≠ SimpleGraph.Walk.nil
• SimpleGraph.Walk.edges_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.edges = p.edges.reverse
• SimpleGraph.Walk.not_nil_of_tail_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.tail.Nil) : ¬p.Nil
• SimpleGraph.Walk.nodup_tail_support_reverse 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup
• SimpleGraph.Walk.support_prefix_support_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : p.support <+: (p.append q).support
• SimpleGraph.Walk.support_prefix_support_concat 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (hadj : G.Adj v w) : p.support <+: (p.concat hadj).support
• SimpleGraph.Walk.support_suffix_support_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : q.support <:+ (p.append q).support
• SimpleGraph.Walk.concat_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
• SimpleGraph.Walk.ext_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (h : p.support = q.support) : p = q
• SimpleGraph.Walk.reverse_toWalk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.reverse = ⋯.toWalk
• SimpleGraph.Walk.edges_dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.dropLast.edges = p.edges.dropLast
• SimpleGraph.Walk.edges_tail 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.tail.edges = p.edges.tail
• SimpleGraph.Walk.nil_drop_of_length_le 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} {p : G.Walk u v} (h : p.length ≤ n) : (p.drop n).Nil
• SimpleGraph.Walk.tail_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {v : V} : SimpleGraph.Walk.nil.tail = SimpleGraph.Walk.nil
• SimpleGraph.Walk.ext_getVert 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) : p = q
• SimpleGraph.Walk.nil_drop_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.drop n).Nil ↔ p.length ≤ n

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c