Loogle!

Result

Found 36 declarations mentioning SimpleGraph.map.

• SimpleGraph.map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W
• SimpleGraph.map_id 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} (G : SimpleGraph V) : SimpleGraph.map (Function.Embedding.refl V) G = G
• SimpleGraph.map_injective 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Function.Injective (SimpleGraph.map f)
• SimpleGraph.Embedding.map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : G ↪g SimpleGraph.map f G
• SimpleGraph.Iso.map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) : G ≃g SimpleGraph.map f.toEmbedding G
• SimpleGraph.map_le_of_subsingleton 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V ↪ W) [Subsingleton V] : SimpleGraph.map f G ≤ G'
• SimpleGraph.leftInverse_comap_map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Function.LeftInverse (SimpleGraph.comap ⇑f) (SimpleGraph.map f)
• SimpleGraph.comap_map_eq 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph.comap (⇑f) (SimpleGraph.map f G) = G
• SimpleGraph.map_comap_le 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.map f (SimpleGraph.comap (⇑f) G) ≤ G
• SimpleGraph.map_map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {X : Type u_3} (G : SimpleGraph V) (f : V ↪ W) (g : W ↪ X) : SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (f.trans g) G
• SimpleGraph.comap_symm 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (e : V ≃ W) : SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map e.toEmbedding G
• SimpleGraph.map_symm 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (G : SimpleGraph W) (e : V ≃ W) : SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G
• SimpleGraph.map_le_iff_le_comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W) : SimpleGraph.map f G ≤ G' ↔ G ≤ SimpleGraph.comap (⇑f) G'
• SimpleGraph.map_monotone 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) : Monotone (SimpleGraph.map f)
• SimpleGraph.map_adj_apply 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {f : V ↪ W} {a b : V} : (SimpleGraph.map f G).Adj (f a) (f b) ↔ G.Adj a b
• SimpleGraph.instDecidableMapAdj 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) {f : V ↪ W} {a b : W} [Decidable (Relation.Map G.Adj (⇑f) (⇑f) a b)] : Decidable ((SimpleGraph.map f G).Adj a b)
• SimpleGraph.Embedding.map_apply 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (v : V) : (SimpleGraph.Embedding.map f G) v = f v
• SimpleGraph.Iso.map_apply 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (v : V) : (SimpleGraph.Iso.map f G) v = f v
• SimpleGraph.map_adj 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (u v : W) : (SimpleGraph.map f G).Adj u v ↔ ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
• SimpleGraph.Iso.map_symm_apply 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph V) (w : W) : (SimpleGraph.Iso.map f G).symm w = f.symm w
• SimpleGraph.cliqueFree_map_iff 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {f : α ↪ β} [Nonempty α] : (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n
• SimpleGraph.IsNClique.map 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {s : Finset α} (h : G.IsNClique n s) {f : α ↪ β} : (SimpleGraph.map f G).IsNClique n (Finset.map f s)
• SimpleGraph.IsClique.finsetMap 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {s : Finset α} (h : G.IsClique ↑s) : (SimpleGraph.map f G).IsClique ↑(Finset.map f s)
• SimpleGraph.IsClique.map 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} (h : G.IsClique s) {f : α ↪ β} : (SimpleGraph.map f G).IsClique (⇑f '' s)
• SimpleGraph.isClique_map_image_iff 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} {f : α ↪ β} : (SimpleGraph.map f G).IsClique (⇑f '' s) ↔ G.IsClique s
• SimpleGraph.cliqueSet_map_of_equiv 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (e : α ≃ β) (n : ℕ) : (SimpleGraph.map e.toEmbedding G).cliqueSet n = Finset.map e.toEmbedding '' G.cliqueSet n
• SimpleGraph.cliqueSet_map 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {n : ℕ} (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) : (SimpleGraph.map f G).cliqueSet n = Finset.map f '' G.cliqueSet n
• SimpleGraph.isClique_map_finset_iff_of_nontrivial 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β} (ht : t.Nontrivial) : (SimpleGraph.map f G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t
• SimpleGraph.isNClique_map_iff 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} (hn : 1 < n) {t : Finset β} {f : α ↪ β} : (SimpleGraph.map f G).IsNClique n t ↔ ∃ s, G.IsNClique n s ∧ Finset.map f s = t
• SimpleGraph.isClique_map_iff_of_nontrivial 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β} (ht : t.Nontrivial) : (SimpleGraph.map f G).IsClique t ↔ ∃ s, G.IsClique s ∧ ⇑f '' s = t
• SimpleGraph.isClique_map_iff 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β} : (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
• SimpleGraph.isClique_map_finset_iff 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β} : (SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ s, G.IsClique ↑s ∧ Finset.map f s = t
• SimpleGraph.cliqueFinset_map 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} [Fintype β] [DecidableEq β] (f : α ↪ β) (hn : n ≠ 1) : (SimpleGraph.map f G).cliqueFinset n = Finset.map { toFun := Finset.map f, inj' := ⋯ } (G.cliqueFinset n)
• SimpleGraph.cliqueFinset_map_of_equiv 📋 Mathlib.Combinatorics.SimpleGraph.Clique
  {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Fintype β] [DecidableEq β] (e : α ≃ β) (n : ℕ) : (SimpleGraph.map e.toEmbedding G).cliqueFinset n = Finset.map { toFun := Finset.map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n)
• SimpleGraph.EdgeDisjointTriangles.map 📋 Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β) (hG : G.EdgeDisjointTriangles) : (SimpleGraph.map f G).EdgeDisjointTriangles
• SimpleGraph.LocallyLinear.map 📋 Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
  {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} (f : α ↪ β) (hG : G.LocallyLinear) : (SimpleGraph.map f G).LocallyLinear

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