Loogle!

Result

Found 138 declarations mentioning SimpleGraph.Walk.IsPath.

• SimpleGraph.Walk.IsPath 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Prop
• SimpleGraph.Walk.IsPath.nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.IsPath
• SimpleGraph.Walk.instDecidableIsPathOfDecidableEq 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : Decidable p.IsPath
• SimpleGraph.Adj.isPath_toWalk 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath
• SimpleGraph.Walk.IsPath.of_adj 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath
• SimpleGraph.Walk.isPath_iff_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.IsPath ↔ p.Nil
• SimpleGraph.Walk.IsPath.isTrail 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (self : p.IsPath) : p.IsTrail
• SimpleGraph.Walk.bypass_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : p.bypass.IsPath
• SimpleGraph.Walk.IsPath.mk' 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.IsPath
• SimpleGraph.Walk.IsPath.support_nodup 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (self : p.IsPath) : p.support.Nodup
• SimpleGraph.Walk.isPath_def 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsPath ↔ p.support.Nodup
• SimpleGraph.Walk.isPath_iff_eq_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.IsPath ↔ p = SimpleGraph.Walk.nil
• SimpleGraph.Walk.IsPath.nil_iff_eq 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.Nil ↔ u = v
• SimpleGraph.Walk.IsPath.reverse 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) : p.reverse.IsPath
• SimpleGraph.Walk.isPath_reverse_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.IsPath ↔ p.IsPath
• SimpleGraph.Walk.IsCycle.isPath_dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) : p.dropLast.IsPath
• SimpleGraph.Walk.IsCycle.isPath_tail 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) : p.tail.IsPath
• SimpleGraph.Walk.IsPath.length_lt 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [Fintype V] {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.length < Fintype.card V
• SimpleGraph.Walk.IsPath.mk 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (isTrail : p.IsTrail) (support_nodup : p.support.Nodup) : p.IsPath
• SimpleGraph.Walk.IsPath.bypass_eq_self 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) : p.bypass = p
• SimpleGraph.Walk.IsPath.dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.dropLast.IsPath
• SimpleGraph.Walk.IsPath.tail 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.tail.IsPath
• SimpleGraph.Path.isPath 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).IsPath
• SimpleGraph.Path.isTrail 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).IsTrail
• SimpleGraph.Walk.bypass_eq_self_iff_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] {p : G.Walk u v} : p.bypass = p ↔ p.IsPath
• SimpleGraph.Path.nil_coe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} : ↑SimpleGraph.Path.nil = SimpleGraph.Walk.nil
• SimpleGraph.Path.nodup_support 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).support.Nodup
• SimpleGraph.Walk.IsPath.drop 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) (n : ℕ) : (p.drop n).IsPath
• SimpleGraph.Walk.IsPath.of_append_left 📋 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).IsPath → p.IsPath
• SimpleGraph.Walk.IsPath.of_append_right 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) : q.IsPath
• SimpleGraph.Walk.IsPath.of_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).IsPath → p.IsPath
• SimpleGraph.Walk.IsPath.take 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) (n : ℕ) : (p.take n).IsPath
• SimpleGraph.Walk.isPath_iff_isSubwalk_imp_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
• SimpleGraph.Walk.isPath_of_isSubwalk 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} (h : p₁.IsSubwalk p₂) (h₂ : p₂.IsPath) : p₁.IsPath
• SimpleGraph.Walk.IsPath.getVert_injOn 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : Set.InjOn p.getVert {i | i ≤ p.length}
• SimpleGraph.Walk.IsPath.mapLe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : p.IsPath → (SimpleGraph.Walk.mapLe h p).IsPath
• SimpleGraph.Walk.IsPath.of_mapLe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsPath → p.IsPath
• SimpleGraph.Walk.isPath_mapLe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath
• SimpleGraph.Walk.mapLe_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath
• SimpleGraph.Walk.IsPath.getVert_injOn_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set.InjOn p.getVert {i | i ≤ p.length} ↔ p.IsPath
• SimpleGraph.Walk.IsCycle.isPath_of_append_left 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬q.Nil) (hcyc : (p.append q).IsCycle) : p.IsPath
• SimpleGraph.Walk.IsCycle.isPath_of_append_right 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬p.Nil) (hcyc : (p.append q).IsCycle) : q.IsPath
• SimpleGraph.Walk.isPath_copy 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {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).IsPath ↔ p.IsPath
• SimpleGraph.Walk.IsCycle.isPath_drop 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {n : ℕ} {p : G.Walk u u} (h : p.IsCycle) (hn : 0 < n) : (p.drop n).IsPath
• SimpleGraph.Walk.IsCycle.isPath_take 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {n : ℕ} {p : G.Walk u u} (h : p.IsCycle) (hn : n < p.length) : (p.take n).IsPath
• SimpleGraph.Walk.IsPath.getVert_eq_start_iff_of_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (h : ¬p.Nil) : p.getVert i = u ↔ i = 0
• SimpleGraph.Walk.IsCycle.isPath_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v w : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) (h : w ∈ c.support) : (c.takeUntil w h).IsPath
• SimpleGraph.Walk.IsTrail.isPath_iff_isSubwalk_imp_not_isCycle 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (ht : p.IsTrail) : p.IsPath ↔ ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → ¬w.IsCycle
• 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.isCycle_iff_isPath_tail_and_le_length 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length
• SimpleGraph.Walk.isPath_iff_injective_get_support 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsPath ↔ Function.Injective fun x => p.support.get x
• SimpleGraph.Walk.IsPath.dropUntil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.dropUntil u h).IsPath
• SimpleGraph.Walk.IsPath.getVert_eq_start_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) : p.getVert i = u ↔ i = 0
• SimpleGraph.Walk.IsPath.takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.takeUntil u h).IsPath
• SimpleGraph.Walk.IsPath.getVert_eq_end_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) : p.getVert i = w ↔ i = p.length
• 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.IsPath.concat 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hw : w ∉ p.support) (h : G.Adj v w) : (p.concat h).IsPath
• SimpleGraph.Walk.IsPath.cons 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : u ∉ p.support) {h : G.Adj u v} : (SimpleGraph.Walk.cons h p).IsPath
• SimpleGraph.Path.singleton_coe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : ↑(SimpleGraph.Path.singleton h) = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
• 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.concat_isPath_iff 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (h : G.Adj v w) : (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support
• SimpleGraph.Walk.cons_isPath_iff 📋 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).IsPath ↔ p.IsPath ∧ u ∉ p.support
• SimpleGraph.Walk.isPath_concat 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (h : G.Adj v w) : (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support
• SimpleGraph.Walk.support_toPath_subset 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).support ⊆ p.support
• SimpleGraph.Walk.support_toPath_subset_support 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).support ⊆ p.support
• SimpleGraph.Walk.IsPath.drop_of_drop 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {n k : ℕ} {p : G.Walk u v} (h : (p.drop k).IsPath) (hle : k ≤ n) : (p.drop n).IsPath
• SimpleGraph.Walk.IsPath.take_of_take 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {n k : ℕ} {p : G.Walk u v} (h : (p.take k).IsPath) (hle : n ≤ k) : (p.take n).IsPath
• 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.darts_toPath_subset 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).darts ⊆ p.darts
• SimpleGraph.Walk.darts_toPath_subset_darts 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) : (↑p.toPath).darts ⊆ p.darts
• 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.endpoint_notMem_support_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w ∈ p.support) (h : v ≠ w) : v ∉ (p.takeUntil w hw).support
• SimpleGraph.Walk.IsPath.disjoint_support_of_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} (hpq : (p.append q).IsPath) (hq : ¬q.Nil) : p.support.Disjoint q.tail.support
• SimpleGraph.Path.reverse_coe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : ↑p.reverse = (↑p).reverse
• 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.IsPath.ne_of_mem_support_of_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} (hpq : (p.append q).IsPath) {x y : V} (hyv : y ≠ v) (hx : x ∈ p.support) (hy : y ∈ q.support) : x ≠ y
• 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.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.Walk.exists_isPath_forall_isPath_length_le_length 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} (G : SimpleGraph V) [N : Nonempty V] [Finite ↑G.edgeSet] : ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
• SimpleGraph.Walk.IsPath.of_map 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hp : (SimpleGraph.Walk.map f p).IsPath) : p.IsPath
• SimpleGraph.Path.count_support_eq_one 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Path u v} (hw : w ∈ (↑p).support) : List.count w (↑p).support = 1
• 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.Walk.IsPath.mem_support_iff_exists_append 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) : w ∈ p.support ↔ ∃ q r, q.IsPath ∧ r.IsPath ∧ p = q.append r
• SimpleGraph.Walk.IsPath.isCycle_append 📋 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) (hq : q.IsPath) (h : p.support.tail.Disjoint q.support.tail) (hn : 1 < p.length ∨ 1 < q.length) : (p.append q).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.map_isPath_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : p.IsPath → (SimpleGraph.Walk.map f p).IsPath
• SimpleGraph.Walk.IsPath.map 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : p.IsPath → (SimpleGraph.Walk.map f p).IsPath
• SimpleGraph.Walk.isPath_map_iff_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath
• SimpleGraph.Walk.map_isPath_iff_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath
• SimpleGraph.Walk.IsPath.exists_isCycle_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (hp : p.IsPath) (hq : q.IsPath) (h : p ≠ q) : ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
• SimpleGraph.Walk.IsPath.injOn_support_of_isPath_map 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} {p : G.Walk u v} {f : G →g G'} (h : (SimpleGraph.Walk.map f p).IsPath) : Set.InjOn ⇑f {w | w ∈ p.support}
• SimpleGraph.Walk.IsPath.exists_isCycle_length_le_add_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (hp : p.IsPath) (hq : q.IsPath) (h : p ≠ q) : ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.length ≤ p.length + q.length
• SimpleGraph.Walk.IsPath.exists_isCycle_sublist_of_ne 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (hp : p.IsPath) (hq : q.IsPath) (h : p ≠ q) : ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.support.Sublist (p.support ++ q.support.reverse.tail)
• SimpleGraph.Path.mapEmbedding_coe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (p : G.Path u v) : ↑(SimpleGraph.Path.mapEmbedding f p) = SimpleGraph.Walk.map f.toHom ↑p
• SimpleGraph.Path.map_coe 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) {u v : V} (p : G.Path u v) : ↑(SimpleGraph.Path.map f hinj p) = SimpleGraph.Walk.map f ↑p
• SimpleGraph.Connected.exists_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} (h : G.Connected) (u v : V) : ∃ p, p.IsPath
• SimpleGraph.Preconnected.exists_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} (h : G.Preconnected) (u v : V) : ∃ p, p.IsPath
• SimpleGraph.Reachable.exists_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ p, p.IsPath
• SimpleGraph.ConnectedComponent.lift 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {β : Sort u_1} (f : V → β) (h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w) : G.ConnectedComponent → β
• SimpleGraph.ConnectedComponent.lift_mk 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {β : Sort u_1} {f : V → β} {h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w} {v : V} : SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f v
• SimpleGraph.ConnectedComponent.recOn 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {motive : G.ConnectedComponent → Sort u_1} (c : G.ConnectedComponent) (f : (v : V) → motive (G.connectedComponentMk v)) (h : ∀ (u v : V) (p : G.Walk u v), p.IsPath → ⋯ ▸ f u = f v) : motive c
• SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v v' : V} {p : G.Walk u v} (hp : p.IsPath) (hadj : p.toSubgraph.Adj u v') : p.snd = v'
• SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) : p.toSubgraph.neighborSet v = {p.penultimate}
• SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) : p.toSubgraph.neighborSet u = {p.snd}
• SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (h : i ≠ 0) (h' : i < p.length) : (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2
• SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (h : i ≠ 0) (h' : i < p.length) : p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}
• SimpleGraph.Walk.isPath_of_length_eq_dist 📋 Mathlib.Combinatorics.SimpleGraph.Metric
  {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : p.length = G.dist u v) : p.IsPath
• SimpleGraph.Connected.exists_path_of_dist 📋 Mathlib.Combinatorics.SimpleGraph.Metric
  {V : Type u_1} {G : SimpleGraph V} (hconn : G.Connected) (u v : V) : ∃ p, p.IsPath ∧ p.length = G.dist u v
• SimpleGraph.Reachable.exists_path_of_dist 📋 Mathlib.Combinatorics.SimpleGraph.Metric
  {V : Type u_1} {G : SimpleGraph V} {u v : V} (hr : G.Reachable u v) : ∃ p, p.IsPath ∧ p.length = G.dist u v
• SimpleGraph.Walk.IsPath.isContained_pathGraph 📋 Mathlib.Combinatorics.SimpleGraph.Hasse
  {V : Type u_3} {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (SimpleGraph.pathGraph (w.length + 1)).IsContained G
• SimpleGraph.Walk.IsPath.pathGraphCopy 📋 Mathlib.Combinatorics.SimpleGraph.Hasse
  {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (SimpleGraph.pathGraph (w.length + 1)).Copy G
• SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraph 📋 Mathlib.Combinatorics.SimpleGraph.Hasse
  {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : SimpleGraph.pathGraph (w.length + 1) ≃g w.toSubgraph.coe
• SimpleGraph.cycleGraph.isPath_tail_cycle 📋 Mathlib.Combinatorics.SimpleGraph.CycleGraph
  {n : ℕ} : (SimpleGraph.cycleGraph.cycle n).tail.IsPath
• SimpleGraph.IsTree.existsUnique_path 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) (v w : V) : ∃! p, p.IsPath
• SimpleGraph.IsAcyclic.isPath_iff_isTrail 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {v w : V} (p : G.Walk v w) : p.IsPath ↔ p.IsTrail
• SimpleGraph.isTree_iff_existsUnique_path 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} : G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath
• 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.IsAcyclic.eq_penultimate_of_adj_end 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hadj : G.Adj v w) (hsupp : w ∈ p.support) : w = p.penultimate
• SimpleGraph.IsAcyclic.eq_snd_of_adj_start 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hadj : G.Adj u w) (hsupp : w ∈ p.support) : w = p.snd
• SimpleGraph.IsAcyclic.mem_support_of_ne_mem_support_of_adj_of_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∉ q.support) : w ∈ p.support
• SimpleGraph.IsAcyclic.ne_mem_support_of_support_of_adj_of_isPath 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hw : w ∈ p.support) : v ∉ q.support
• SimpleGraph.IsAcyclic.path_concat 📋 Mathlib.Combinatorics.SimpleGraph.Acyclic
  {V : Type u_1} {G : SimpleGraph V} (hG : G.IsAcyclic) {u v w : V} {p : G.Walk u v} {q : G.Walk u w} (hp : p.IsPath) (hq : q.IsPath) (hadj : G.Adj v w) (hv : v ∈ q.support) : q = p.concat hadj
• SimpleGraph.fintypeSubtypePathLength 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Counting
  {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p // p.IsPath ∧ p.length = n }
• SimpleGraph.fintypeSubtypePathLengthLT 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Counting
  {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p // p.IsPath ∧ p.length < n }
• SimpleGraph.fintypeSetPathLength 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Counting
  {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p | p.IsPath ∧ p.length = n}
• SimpleGraph.fintypeSetPathLengthLT 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Counting
  {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p | p.IsPath ∧ p.length < n}
• SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe 📋 Mathlib.Combinatorics.SimpleGraph.Matching
  {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w : V} (hcyc : G.IsCycles) (p : G.Walk v w) (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v
• SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj 📋 Mathlib.Combinatorics.SimpleGraph.Matching
  {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w w' : V} (hcyc : G.IsCycles) (p : G.Walk v w) (hw : w ≠ w') (hw' : w' ∈ p.support) (hp : p.IsPath) (hadj : G.Adj v w') : p.snd = w'
• 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.IsHamiltonian.isPath 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) : p.IsPath
• SimpleGraph.Walk.IsPath.isHamiltonian_of_mem 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsPath) (hp' : ∀ (w : α), w ∈ p.support) : p.IsHamiltonian
• SimpleGraph.Walk.IsPath.isHamiltonian_iff 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsPath) : p.IsHamiltonian ↔ ∀ (w : α), w ∈ p.support
• SimpleGraph.Walk.isHamiltonian_iff_isPath_and_length_eq 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} [Fintype α] : p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1
• SimpleGraph.Walk.IsHamiltonian.injective_of_isPath_map 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} [DecidableEq α] {G : SimpleGraph α} {β : Type u_2} {H : SimpleGraph β} {a b : α} {p : G.Walk a b} {f : G →g H} (hp : p.IsHamiltonian) (h : (SimpleGraph.Walk.map f p).IsPath) : Function.Injective ⇑f

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