Loogle!

Result

Found 34 declarations mentioning SimpleGraph.Walk.map.

• SimpleGraph.Walk.map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} : G.Walk u v → G'.Walk (f u) (f v)
• SimpleGraph.Walk.map_id 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : SimpleGraph.Walk.map SimpleGraph.Hom.id p = p
• SimpleGraph.Walk.transfer_eq_map_ofLE 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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.transfer_eq_map_of_le 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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.length_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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).length = p.length
• SimpleGraph.Walk.map_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} : SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
• SimpleGraph.Walk.map_injective_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u v : V) : Function.Injective (SimpleGraph.Walk.map f)
• SimpleGraph.Walk.darts_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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).darts = List.map f.mapDart p.darts
• SimpleGraph.Walk.support_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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).support = List.map (⇑f) p.support
• SimpleGraph.Walk.map_eq_nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u} : SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil ↔ p = SimpleGraph.Walk.nil
• SimpleGraph.Walk.edgeSet_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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).edgeSet = Sym2.map ⇑f '' p.edgeSet
• SimpleGraph.Walk.edges_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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.reverse_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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).reverse = SimpleGraph.Walk.map f p.reverse
• SimpleGraph.Walk.map_toDeleteEdges_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {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.map_append 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)
• SimpleGraph.Walk.map_cons 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) : SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
• SimpleGraph.Walk.map_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u v : V} (p : G.Walk u v) : SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (f'.comp f) p
• SimpleGraph.Walk.map_copy 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy ⋯ ⋯
• SimpleGraph.Walk.map_eq_of_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') : SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).copy ⋯ ⋯
• SimpleGraph.Walk.IsCycle.map 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : p.IsCycle → (SimpleGraph.Walk.map f p).IsCycle
• SimpleGraph.Walk.IsPath.of_map 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} {p : G.Walk u v} {f : G →g G'} (hp : (SimpleGraph.Walk.map f p).IsPath) : p.IsPath
• SimpleGraph.Walk.map_isCycle_iff_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle
• SimpleGraph.Walk.map_isPath_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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) (hp : p.IsPath) : (SimpleGraph.Walk.map f p).IsPath
• SimpleGraph.Walk.map_isTrail_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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.IsTrail → (SimpleGraph.Walk.map f p).IsTrail
• SimpleGraph.Walk.map_isPath_iff_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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_isTrail_iff_of_injective 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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).IsTrail ↔ p.IsTrail
• SimpleGraph.Path.mapEmbedding_coe 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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.Path
  {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.Path.map.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Path
  {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.Walk.boxProdLeft.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Prod
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (H : SimpleGraph β) {a₁ a₂ : α} (b : β) : SimpleGraph.Walk.boxProdLeft H b = SimpleGraph.Walk.map (G.boxProdLeft H b).toHom
• SimpleGraph.Walk.boxProdRight.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Prod
  {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) {H : SimpleGraph β} {b₁ b₂ : β} (a : α) : SimpleGraph.Walk.boxProdRight G a = SimpleGraph.Walk.map (G.boxProdRight H a).toHom
• SimpleGraph.Walk.toSubgraph_map 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (f : G →g G') (p : G.Walk u v) : (SimpleGraph.Walk.map f p).toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph
• SimpleGraph.Walk.IsHamiltonianCycle.map 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {G : SimpleGraph α} {a : α} {p : G.Walk a a} {H : SimpleGraph β} (f : G →g H) (hf : Function.Bijective ⇑f) (hp : p.IsHamiltonianCycle) : (SimpleGraph.Walk.map f p).IsHamiltonianCycle
• SimpleGraph.Walk.IsHamiltonian.map 📋 Mathlib.Combinatorics.SimpleGraph.Hamiltonian
  {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} {H : SimpleGraph β} (f : G →g H) (hf : Function.Bijective ⇑f) (hp : p.IsHamiltonian) : (SimpleGraph.Walk.map f p).IsHamiltonian

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65