Loogle!

Result

Found 46 declarations mentioning SimpleGraph.Walk.map.

SimpleGraph.Walk.map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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.Walks.Maps
{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.Walks.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.length_map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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).length = p.length
SimpleGraph.Walk.map_nil 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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.Walks.Maps
{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.Walks.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).darts = List.map f.mapDart p.darts
SimpleGraph.Walk.getVert_map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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) (n : ℕ) : (SimpleGraph.Walk.map f p).getVert n = f (p.getVert n)
SimpleGraph.Walk.support_map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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).support = List.map (⇑f) p.support
SimpleGraph.Walk.map_eq_nil_iff 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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.Walks.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).edgeSet = Sym2.map ⇑f '' p.edgeSet
SimpleGraph.Walk.edges_map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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.reverse_map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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).reverse = SimpleGraph.Walk.map f p.reverse
SimpleGraph.Walk.map_toDeleteEdges_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walks.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.map_append 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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.Walks.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) {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.Walks.Maps
{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.hcongr_8 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
(V V' : Type u) (e_1 : V = V') (V'✝ V'' : Type v) (e_2 : V'✝ = V'') (G : SimpleGraph V) (G' : SimpleGraph V') (e_3 : G ≍ G') (G'✝ : SimpleGraph V'✝) (G'' : SimpleGraph V'') (e_4 : G'✝ ≍ G'') (f : G →g G'✝) (f' : G' →g G'') (e_5 : f ≍ f') (u : V) (u' : V') (e_6 : u ≍ u') (v : V) (v' : V') (e_7 : v ≍ v') (a✝ : G.Walk u v) (a'✝ : G'.Walk u' v') (e_8 : a✝ ≍ a'✝) : SimpleGraph.Walk.map f a✝ ≍ SimpleGraph.Walk.map f' a'✝
SimpleGraph.Walk.map_induce 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{V : Type u} {G : SimpleGraph V} {s : Set V} {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : SimpleGraph.Walk.map (SimpleGraph.Embedding.induce s).toHom (SimpleGraph.Walk.induce s w hw) = w
SimpleGraph.Walk.map_copy 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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_induce_induceHomOfLE 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{V : Type u} {G : SimpleGraph V} {s s' : Set V} (hs : s ⊆ s') {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : SimpleGraph.Walk.map (G.induceHomOfLE hs).toHom (SimpleGraph.Walk.induce s w hw) = SimpleGraph.Walk.induce s' w ⋯
SimpleGraph.Walk.map_eq_of_eq 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Maps
{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.IsSubwalk.map 📋 Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks
{V : Type u_1} {G G' : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) (f : G →g G') : (SimpleGraph.Walk.map f p₂).IsSubwalk (SimpleGraph.Walk.map f p₁)
SimpleGraph.Walk.IsCycle.map 📋 Mathlib.Combinatorics.SimpleGraph.Paths
{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.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'} (hp : (SimpleGraph.Walk.map f p).IsPath) : p.IsPath
SimpleGraph.Walk.map_isCycle_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} {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.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) (hp : p.IsPath) : (SimpleGraph.Walk.map f p).IsPath
SimpleGraph.Walk.map_isTrail_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.IsTrail → (SimpleGraph.Walk.map f p).IsTrail
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.map_isTrail_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).IsTrail ↔ p.IsTrail
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.Path.map.eq_1 📋 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.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.map.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{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.eq_2 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v) : SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
SimpleGraph.Walk.map.eq_def 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (x✝ : G.Walk u v) : SimpleGraph.Walk.map f x✝ = match v, x✝ with | .(u), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil | v, SimpleGraph.Walk.cons h p => SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)
SimpleGraph.Walk.map_mapToSubgraph_hom 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : SimpleGraph.Walk.map w.toSubgraph.hom w.mapToSubgraph = w
SimpleGraph.Walk.mapToSubgraph.eq_2 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (p : G.Walk v_3 v) : (SimpleGraph.Walk.cons h p).mapToSubgraph = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map (SimpleGraph.Subgraph.inclusion ⋯) p.mapToSubgraph)
SimpleGraph.Walk.mapToSubgraph.eq_def 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {G : SimpleGraph V} {u v : V} (x✝ : G.Walk u v) : x✝.mapToSubgraph = match v, x✝ with | .(u), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil | v, SimpleGraph.Walk.cons h p => have h_1 := ⋯; have h_2 := h_1; SimpleGraph.Walk.cons h_2 (SimpleGraph.Walk.map (SimpleGraph.Subgraph.inclusion ⋯) p.mapToSubgraph)
SimpleGraph.Walk.map_mapToSubgraph_eq_induce 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {G : SimpleGraph V} (s : Set V) {u v : V} (w : G.Walk u v) (hs : ∀ x ∈ w.support, x ∈ s) : SimpleGraph.Walk.map { toFun := fun x => ⟨↑x, ⋯⟩, map_rel' := ⋯ } w.mapToSubgraph = SimpleGraph.Walk.induce s w hs
SimpleGraph.Walk.map_mapToSubgraph_eq_induce_id 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
{V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : SimpleGraph.Walk.map { toFun := fun v_1 => ⟨↑v_1, ⋯⟩, map_rel' := ⋯ } w.mapToSubgraph = SimpleGraph.Walk.induce (fun x => List.Mem x w.support) w ⋯
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.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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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 6ff4759 serving mathlib revision edaf32c