Loogle!
Result
Found 1984 definitions mentioning SimpleGraph. Of these, 32 match your pattern(s).
- completeGraph 📋 Mathlib.Combinatorics.SimpleGraph.Basic
(V : Type u) : SimpleGraph V - emptyGraph 📋 Mathlib.Combinatorics.SimpleGraph.Basic
(V : Type u) : SimpleGraph V - completeBipartiteGraph 📋 Mathlib.Combinatorics.SimpleGraph.Basic
(V : Type u_1) (W : Type u_2) : SimpleGraph (V ⊕ W) - SimpleGraph.fromEdgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Basic
{V : Type u} (s : Set (Sym2 V)) : SimpleGraph V - SimpleGraph.fromRel 📋 Mathlib.Combinatorics.SimpleGraph.Basic
{V : Type u} (r : V → V → Prop) : SimpleGraph V - SimpleGraph.deleteEdges 📋 Mathlib.Combinatorics.SimpleGraph.Basic
{V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph V - SimpleGraph.mk 📋 Mathlib.Combinatorics.SimpleGraph.Basic
{V : Type u} (Adj : V → V → Prop) (symm : Symmetric Adj := by aesop_graph) (loopless : Irreflexive Adj := by aesop_graph) : SimpleGraph V - SimpleGraph.regularityReduced 📋 Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
{α : Type u_1} {𝕜 : Type u_2} [LinearOrderedField 𝕜] [DecidableEq α] {A : Finset α} (P : Finpartition A) (G : SimpleGraph α) [DecidableRel G.Adj] (ε δ : 𝕜) : SimpleGraph α - SimpleGraph.comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : SimpleGraph V - SimpleGraph.completeMultipartiteGraph 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{ι : Type u_4} (V : ι → Type u_5) : SimpleGraph ((i : ι) × V i) - SimpleGraph.induce 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{V : Type u_1} (s : Set V) (G : SimpleGraph V) : SimpleGraph ↑s - SimpleGraph.map 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W - SimpleGraph.spanningCoe 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{V : Type u_1} {s : Set V} (G : SimpleGraph ↑s) : SimpleGraph V - SimpleGraph.overFin 📋 Mathlib.Combinatorics.SimpleGraph.Maps
{V : Type u_1} (G : SimpleGraph V) [Fintype V] {n : ℕ} (hc : Fintype.card V = n) : SimpleGraph (Fin n) - SimpleGraph.Subgraph.spanningCoe 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
{V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) : SimpleGraph V - SimpleGraph.Subgraph.coe 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
{V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) : SimpleGraph ↑G'.verts - SimpleGraph.edge 📋 Mathlib.Combinatorics.SimpleGraph.Operations
{V : Type u_1} (s t : V) : SimpleGraph V - SimpleGraph.replaceVertex 📋 Mathlib.Combinatorics.SimpleGraph.Operations
{V : Type u_1} (G : SimpleGraph V) (s t : V) [DecidableEq V] : SimpleGraph V - SimpleGraph.TripartiteFromTriangles.graph 📋 Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
{α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : SimpleGraph (α ⊕ β ⊕ γ) - Digraph.toSimpleGraphInclusive 📋 Mathlib.Combinatorics.Digraph.Orientation
{V : Type u_1} (G : Digraph V) : SimpleGraph V - Digraph.toSimpleGraphStrict 📋 Mathlib.Combinatorics.Digraph.Orientation
{V : Type u_1} (G : Digraph V) : SimpleGraph V - Matrix.IsAdjMatrix.toGraph 📋 Mathlib.Combinatorics.SimpleGraph.AdjMatrix
{V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) : SimpleGraph V - SimpleGraph.boxProd 📋 Mathlib.Combinatorics.SimpleGraph.Prod
{α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α × β) - SimpleGraph.pathGraph 📋 Mathlib.Combinatorics.SimpleGraph.Hasse
(n : ℕ) : SimpleGraph (Fin n) - SimpleGraph.hasse 📋 Mathlib.Combinatorics.SimpleGraph.Hasse
(α : Type u_1) [Preorder α] : SimpleGraph α - SimpleGraph.cycleGraph 📋 Mathlib.Combinatorics.SimpleGraph.Circulant
(n : ℕ) : SimpleGraph (Fin n) - SimpleGraph.circulantGraph 📋 Mathlib.Combinatorics.SimpleGraph.Circulant
{G : Type u_1} [AddGroup G] (s : Set G) : SimpleGraph G - SimpleGraph.ComponentCompl.coeGraph 📋 Mathlib.Combinatorics.SimpleGraph.Ends.Defs
{V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K) : SimpleGraph ↥C - SimpleGraph.lineGraph 📋 Mathlib.Combinatorics.SimpleGraph.LineGraph
{V : Type u_2} (G : SimpleGraph V) : SimpleGraph ↑G.edgeSet - SimpleGraph.sum 📋 Mathlib.Combinatorics.SimpleGraph.Sum
{α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α ⊕ β) - SimpleGraph.turanGraph 📋 Mathlib.Combinatorics.SimpleGraph.Turan
(n r : ℕ) : SimpleGraph (Fin n) - FirstOrder.Language.simpleGraphOfStructure 📋 Mathlib.ModelTheory.Graph
(V : Type u) [FirstOrder.Language.graph.Structure V] [V ⊨ FirstOrder.Language.Theory.simpleGraph] : SimpleGraph V
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 findtsum_lt_tsum
even though the hypothesisf 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 4e1aab0
serving mathlib revision 83ce5b0