Loogle!

Result

Found 98 declarations mentioning SimpleGraph.Walk.Nil.

• SimpleGraph.Walk.Nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {v w : V} : G.Walk v w → Prop
• SimpleGraph.Walk.nil_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.Nil
• SimpleGraph.Walk.Nil.nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.Nil
• 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.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.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.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.exists_nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Basic
  {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ p, p.Nil) ↔ u = v
• 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.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.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.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.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.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.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_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.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.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.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.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.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.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.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.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.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.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.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.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.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
• SimpleGraph.Walk.Nil.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} (hp : p.Nil) (hq : q.Nil) : (p.append q).Nil
• SimpleGraph.Walk.nil_append_iff 📋 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.append q).Nil ↔ p.Nil ∧ q.Nil
• SimpleGraph.Walk.nil_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).Nil = p.Nil
• SimpleGraph.Walk.support_dropLast 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.support = p.support.dropLast
• SimpleGraph.Walk.support_tail_of_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) : p.tail.support = p.support.tail
• SimpleGraph.Walk.Nil.eq_copy_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.Nil) : p = SimpleGraph.Walk.nil.copy ⋯ ⋯
• SimpleGraph.Walk.cons_support_tail 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : u :: p.tail.support = p.support
• SimpleGraph.Walk.nil_take_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.take n).Nil ↔ p.Nil ∨ n = 0
• SimpleGraph.Walk.getVert_mem_tail_support 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) {i : ℕ} : i ≠ 0 → p.getVert i ∈ p.support.tail
• SimpleGraph.Walk.cons_tail_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) : SimpleGraph.Walk.cons ⋯ p.tail = p
• SimpleGraph.Walk.length_dropLast_add_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.length + 1 = p.length
• SimpleGraph.Walk.length_tail_add_one 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : p.tail.length + 1 = p.length
• SimpleGraph.Walk.support_dropLast_concat 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : p.dropLast.support ++ [v] = p.support
• SimpleGraph.Walk.dropLast_cons_of_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {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).dropLast = SimpleGraph.Walk.cons h (p.dropLast.copy ⋯ ⋯)
• SimpleGraph.Walk.ofDarts_darts 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Operations
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) : SimpleGraph.Walk.ofDarts p.darts ⋯ ⋯ = p.copy ⋯ ⋯
• SimpleGraph.Walk.nil_map_iff 📋 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).Nil ↔ p.Nil
• SimpleGraph.Walk.isSubwalk_iff_darts_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'} (hnil : ¬p₁.Nil) : p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts
• SimpleGraph.Walk.nil_rotate 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {c : G.Walk v v} (h : u ∈ c.support) : (c.rotate u h).Nil ↔ c.Nil
• SimpleGraph.Walk.nil_takeUntil 📋 Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
  {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk u v) (hwp : w ∈ p.support) : (p.takeUntil w hwp).Nil ↔ u = w
• SimpleGraph.Walk.IsCircuit.not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCircuit) : ¬p.Nil
• SimpleGraph.Walk.IsCycle.not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) : ¬p.Nil
• 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.nil_bypass 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u : V} [DecidableEq V] (p : G.Walk u u) : p.bypass.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.not_nil_of_isCycle_cons 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {h : G.Adj v u} (hc : (SimpleGraph.Walk.cons h p).IsCycle) : ¬p.Nil
• 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.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.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.IsTrail.cycleBypass_eq_self_iff_isCycle_or_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] {w : G.Walk v v} (hw : w.IsTrail) : w.cycleBypass = w ↔ w.IsCycle ∨ w.Nil
• SimpleGraph.Walk.IsTrail.length_cycleBypass_lt_iff_not_isCycle_and_not_nil 📋 Mathlib.Combinatorics.SimpleGraph.Paths
  {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] {w : G.Walk v v} (hw : w.IsTrail) : w.cycleBypass.length < w.length ↔ ¬w.IsCycle ∧ ¬w.Nil
• 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.mem_support_of_mem_walk_support 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {w : V} (hw : w ∈ p.support) : w ∈ G.support
• SimpleGraph.adj_of_mem_walk_support 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : ¬p.Nil) {x : V} (hx : x ∈ p.support) : ∃ y ∈ p.support, G.Adj x y
• SimpleGraph.Walk.not_nil_of_adj_toSubgraph 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {w u v x : V} {p : G.Walk u v} (hadj : p.toSubgraph.Adj w x) : ¬p.Nil
• SimpleGraph.Walk.toSubgraph_adj_penultimate 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj w.penultimate v
• SimpleGraph.Walk.toSubgraph_adj_snd 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj u w.snd
• 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.toSubgraph_le_iff 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hnil : ¬w.Nil) {G' : G.Subgraph} : w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet
• SimpleGraph.Walk.IsEulerian.nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} [DecidableEq V] (hp : p.IsEulerian) : p.Nil ↔ G = ⊥
• SimpleGraph.Walk.IsEulerian.mem_support_iff 📋 Mathlib.Combinatorics.SimpleGraph.Trails
  {V : Type u_1} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} [DecidableEq V] (hp : p.IsEulerian) (hnil : ¬p.Nil) : w ∈ p.support ↔ ¬G.IsIsolated w

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