Loogle!

Result

Found 124 declarations mentioning SimpleGraph.Walk.edges.

• 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.edges_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.edges
• SimpleGraph.Walk.edges_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.edges = []
• 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.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.Adj.edges_toWalk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.edges = [s(u, v)]
• 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.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.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.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.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.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.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.edges_ofDarts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {l : List G.Dart} (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l) : (SimpleGraph.Walk.ofDarts l hne hchain).edges = List.map SimpleGraph.Dart.edge l
• 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.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.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.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.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.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.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.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.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.edges_drop 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.drop n).edges = List.drop n p.edges
• SimpleGraph.Walk.edges_take 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.take n).edges = List.take n p.edges
• SimpleGraph.Walk.fst_mem_support_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) : t ∈ p.support
• SimpleGraph.Walk.snd_mem_support_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) : u ∈ p.support
• SimpleGraph.Walk.edges_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') : (p.copy hu hv).edges = p.edges
• SimpleGraph.Walk.edges_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) : (p.concat h).edges = p.edges.concat s(v, w)
• SimpleGraph.Walk.mem_support_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} {e : Sym2 V} {p : G.Walk u v} (he : e ∈ p.edges) (hv : w ∈ e) : w ∈ p.support
• SimpleGraph.Walk.edges_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').edges = p.edges ++ p'.edges
• SimpleGraph.Walk.edges_mapLe_eq_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.mapLe h p).edges = p.edges
• SimpleGraph.Walk.toDeleteEdge 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {v w : V} (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) : (G.deleteEdges {e}).Walk v w
• SimpleGraph.Walk.transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e ∈ p.edges, e ∈ H.edgeSet) : H.Walk u v
• SimpleGraph.Walk.toDeleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v w : V} (p : G.Walk v w) (hp : ∀ e ∈ p.edges, e ∉ s) : (G.deleteEdges s).Walk v w
• SimpleGraph.Walk.length_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).length = p.length
• SimpleGraph.Walk.support_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).support = p.support
• SimpleGraph.Walk.edgeSet_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edgeSet = p.edgeSet
• SimpleGraph.Walk.edges_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edges = p.edges
• SimpleGraph.Walk.toDeleteEdges_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil
• SimpleGraph.Walk.transfer_eq_map_ofLE 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (GH : G ≤ H) : p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.ofLE GH) p
• SimpleGraph.Walk.reverse_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).reverse = p.reverse.transfer H ⋯
• SimpleGraph.Walk.edges_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges
• SimpleGraph.Walk.map_toDeleteEdges_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s) : SimpleGraph.Walk.map (SimpleGraph.Hom.ofLE ⋯) (SimpleGraph.Walk.toDeleteEdges s p hp) = p
• SimpleGraph.Walk.transfer_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w) (hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet) : (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
• SimpleGraph.Walk.transfer_transfer 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) {K : SimpleGraph V} (hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet) : (p.transfer H hp).transfer K hp' = p.transfer K ⋯
• SimpleGraph.Walk.toDeleteEdges_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Maps
  {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ∀ e ∈ (SimpleGraph.Walk.cons h p).edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toDeleteEdges s p ⋯)
• SimpleGraph.Walk.IsSubwalk.edges_isInfix 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
  {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₁.IsSubwalk p₂) : p₁.edges <:+: p₂.edges
• SimpleGraph.Walk.IsSubwalk.edges_subset 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
  {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) : p₂.edges ⊆ p₁.edges
• SimpleGraph.Walk.infix_support_iff_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
  {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges
• SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
  {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : G.Adj u' v') : h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges
• SimpleGraph.Walk.rotate_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] (c : G.Walk v v) (u : V) (h : u ∈ c.support) : (c.rotate u h).edges ~r c.edges
• SimpleGraph.Walk.edges_dropUntil_suffix_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges <:+ p.edges
• SimpleGraph.Walk.edges_takeUntil_prefix_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges <+: p.edges
• SimpleGraph.Walk.edges_dropUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.edges_dropUntil_subset_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.edges_takeUntil_subset 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.edges_takeUntil_subset_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges
• SimpleGraph.Walk.count_edges_takeUntil_le_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) : List.count s(u, x) (p.takeUntil u h).edges ≤ 1
• SimpleGraph.Walk.IsTrail.edges_nodup 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (self : p.IsTrail) : p.edges.Nodup
• SimpleGraph.Walk.IsTrail.mk 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (edges_nodup : p.edges.Nodup) : p.IsTrail
• SimpleGraph.Walk.isTrail_def 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsTrail ↔ p.edges.Nodup
• SimpleGraph.Walk.edges_cycleBypass_sublist_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] (w : G.Walk v v) : w.cycleBypass.edges.Sublist w.edges
• SimpleGraph.Walk.edges_bypass_sublist_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : p.bypass.edges.Sublist p.edges
• SimpleGraph.Walk.edges_cycleBypass_subset 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] (w : G.Walk v v) : w.cycleBypass.edges ⊆ w.edges
• SimpleGraph.Walk.edges_cycleBypass_subset_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] (w : G.Walk v v) : w.cycleBypass.edges ⊆ w.edges
• SimpleGraph.Walk.edges_bypass_subset 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : p.bypass.edges ⊆ p.edges
• SimpleGraph.Walk.edges_bypass_subset_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : p.bypass.edges ⊆ p.edges
• SimpleGraph.Path.notMem_edges_of_loop 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} : e ∉ (↑p).edges
• SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hmem : s(v, w) ∈ p.edges) : w = p.penultimate
• SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hmem : s(u, w) ∈ p.edges) : w = p.snd
• SimpleGraph.Walk.IsPath.length_eq_one_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : s(u, v) ∈ p.edges) : p.length = 1
• SimpleGraph.Walk.IsTrail.count_edges_le_one 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) : List.count e p.edges ≤ 1
• SimpleGraph.Path.mk'_mem_edges_singleton 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : s(u, v) ∈ (↑(SimpleGraph.Path.singleton h)).edges
• SimpleGraph.Walk.edges_toPath_subset 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).edges ⊆ p.edges
• SimpleGraph.Walk.edges_toPath_subset_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).edges ⊆ p.edges
• SimpleGraph.Walk.cons_isCycle_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk v u) (h : G.Adj u v) : (SimpleGraph.Walk.cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges
• SimpleGraph.Walk.IsTrail.concat 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsTrail) (hadj : G.Adj v w) (hmem : s(v, w) ∉ p.edges) : (p.concat hadj).IsTrail
• SimpleGraph.Walk.IsTrail.cons 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u u' v : V} {w : G.Walk u' v} (hw : w.IsTrail) (hu : G.Adj u u') (hu' : s(u, u') ∉ w.edges) : (SimpleGraph.Walk.cons hu w).IsTrail
• SimpleGraph.Walk.IsPath.eq_adj_toWalk_of_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : s(u, v) ∈ p.edges) : p = ⋯.toWalk
• SimpleGraph.Walk.isTrail_concat 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hadj : G.Adj v w) : (p.concat hadj).IsTrail ↔ p.IsTrail ∧ s(v, w) ∉ p.edges
• SimpleGraph.Walk.isTrail_cons 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {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).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges
• SimpleGraph.Walk.isTrail_append 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).IsTrail ↔ p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges
• SimpleGraph.Walk.IsCycle.transfer 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {H : SimpleGraph V} {q : G.Walk u u} (qc : q.IsCycle) (hq : ∀ e ∈ q.edges, e ∈ H.edgeSet) : (q.transfer H hq).IsCycle
• SimpleGraph.Walk.IsCycle.toDeleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} (G : SimpleGraph V) {v : V} (s : Set (Sym2 V)) {p : G.Walk v v} (h : p.IsCycle) (hp : ∀ e ∈ p.edges, e ∉ s) : (SimpleGraph.Walk.toDeleteEdges s p hp).IsCycle
• SimpleGraph.Walk.IsPath.transfer 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {H : SimpleGraph V} {p : G.Walk u v} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (pp : p.IsPath) : (p.transfer H hp).IsPath
• SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] {x : V} {w : G.Walk u v} (hw : w.IsTrail) (hx : x ∈ w.support) : (w.takeUntil x hx).edges.Disjoint (w.dropUntil x hx).edges
• SimpleGraph.Walk.IsPath.toDeleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} (G : SimpleGraph V) {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp : ∀ e ∈ p.edges, e ∉ s) : (SimpleGraph.Walk.toDeleteEdges s p hp).IsPath
• SimpleGraph.Walk.IsTrail.count_edges_eq_one 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e ∈ p.edges) : List.count e p.edges = 1
• SimpleGraph.Walk.IsPath.disjoint_edges_of_disjoint_support 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (hp : p.IsPath) (hd : p.support.tail.Disjoint q.support.tail) (hl : p.length ≠ 1) : p.edges.Disjoint q.edges
• SimpleGraph.Path.cons_isCycle 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v) ∉ (↑p).edges) : (SimpleGraph.Walk.cons h ↑p).IsCycle
• SimpleGraph.Path.count_edges_eq_one 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Path u v} (e : Sym2 V) (hw : e ∈ (↑p).edges) : List.count e (↑p).edges = 1
• SimpleGraph.Walk.toDeleteEdges_copy 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} (G : SimpleGraph V) {v u u' v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = (SimpleGraph.Walk.toDeleteEdges s p ⋯).copy hu hv
• SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {v w : V} : G.IsBridge s(v, w) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
• SimpleGraph.isBridge_iff_forall_walk_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {v w : V} : G.IsBridge s(v, w) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
• SimpleGraph.IsBridge.notMem_edges_of_isCycle 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {e : Sym2 V} {u : V} {p : G.Walk u u} (he : G.IsBridge e) (hp : p.IsCycle) : e ∉ p.edges
• SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {e : Sym2 V} (huv : ¬(G.deleteEdges {e}).Reachable u v) : e ∈ w.edges
• SimpleGraph.isBridge_iff_adj_and_forall_cycle_notMem 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {e : Sym2 V} (he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges
• SimpleGraph.isBridge_iff_forall_cycle_notMem 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {e : Sym2 V} (he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges
• SimpleGraph.isBridge_iff_mem_and_forall_cycle_notMem 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {e : Sym2 V} (he : e ∈ G.edgeSet) : G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges
• SimpleGraph.Walk.exists_mem_edges_of_not_reachable_deleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {s : Set (Sym2 V)} (huv : ¬(G.deleteEdges s).Reachable u v) : ∃ e ∈ s, e ∈ w.edges
• SimpleGraph.reachable_deleteEdges_iff_exists_walk 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {v w v' w' : V} : (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ p, s(v, w) ∉ p.edges
• SimpleGraph.reachable_delete_edges_iff_exists_walk 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {v w v' w' : V} : (G.deleteEdges {s(v, w)}).Reachable v' w' ↔ ∃ p, s(v, w) ∉ p.edges
• SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {v w : V} : G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
• SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_reachable 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v x y : V} {w : G.Walk u v} (hw : w.IsTrail) (huy : ¬(G.deleteEdges {s(x, y)}).Reachable u y) (hvy : ¬(G.deleteEdges {s(x, y)}).Reachable v y) : s(x, y) ∉ w.edges
• SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges) (c : G.Walk u u) (hc : c.IsTrail) (he : s(v, w) ∈ c.edges) (hw : w ∈ (c.takeUntil v ⋯).support) : False
• SimpleGraph.Walk.IsChordless.mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Chord
  {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsChordless) {u' v' : V} (hu' : u' ∈ p.support) (hv' : v' ∈ p.support) (hadj : G.Adj u' v') : s(u', v') ∈ p.edges
• SimpleGraph.Walk.isChordless_iff_forall_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Chord
  {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.IsChordless ↔ ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges
• SimpleGraph.Walk.isChord_sym2Mk 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Chord
  {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {u' v' : V} : p.IsChord s(u', v') ↔ G.Adj u' v' ∧ s(u', v') ∉ p.edges ∧ u' ∈ p.support ∧ v' ∈ p.support
• SimpleGraph.Walk.adj_toSubgraph_iff_mem_edges 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} : p.toSubgraph.Adj u' v' ↔ s(u', v') ∈ p.edges
• SimpleGraph.Walk.mem_edges_toSubgraph 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {e : Sym2 V} : e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges
• SimpleGraph.IsAcyclic.isPath_iff_isChain 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) : p.IsPath ↔ List.IsChain (fun x1 x2 => x1 ≠ x2) p.edges
• SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge 📋 Mathlib.Combinatorics.SimpleGraph.Matching
  {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (h : u ≠ v) (hs : s(v, u) ∉ p.edges) : (p.toSubgraph.spanningCoe ⊔ SimpleGraph.edge v u).IsCycles
• SimpleGraph.Walk.IsEulerian.mem_edges_iff 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} : e ∈ p.edges ↔ e ∈ G.edgeSet
• SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (hc : ∀ e ∈ G.edgeSet, e ∈ p.edges) : p.IsEulerian
• SimpleGraph.Walk.isEulerian_iff 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.IsEulerian ↔ p.IsTrail ∧ ∀ e ∈ G.edgeSet, e ∈ p.edges
• SimpleGraph.Walk.IsTrail.even_countP_edges_iff 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

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