Mathlib Map

Theorems · Definition · combinatorics

SimpleGraph.fromEdgeSet

{V : Type u} → Set (Sym2 V) → SimpleGraph V

fromEdgeSet constructs a SimpleGraph from a set of edges, without loops.

Defined in
Mathlib.Combinatorics.SimpleGraph.Basic
Cited by
43 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimpleGraph.deleteEdges · cited by 64SimpleGraph.deleteEdgesSimpleGraph.edge · cited by 44SimpleGraph.edgeSimpleGraph.edgeSet_fromEdgeSet · cited by 17SimpleGraph.edgeSet_fromE…SimpleGraph.EdgeLabeling.labelGraph · cited by 9EdgeLabeling.labelGraphSimpleGraph.measurableEmbedding_edgeSet · cited by 3SimpleGraph.measurableEmb…SimpleGraph.edgeSet_deleteEdges · cited by 3SimpleGraph.edgeSet_delet…SimpleGraph.fromEdgeSet_empty · cited by 3SimpleGraph.fromEdgeSet_e…SimpleGraph.measurable_fromEdgeSet · cited by 2SimpleGraph.measurable_fr…SimpleGraph.deleteEdges_deleteEdges · cited by 2SimpleGraph.deleteEdges_d…SimpleGraph.deleteEdges_edge · cited by 2SimpleGraph.deleteEdges_e…SimpleGraph.deleteEdges_fromEdgeSet · cited by 2SimpleGraph.deleteEdges_f…SimpleGraph.edge_comm · cited by 2SimpleGraph.edge_commSimpleGraph.disjoint_fromEdgeSet · cited by 2SimpleGraph.disjoint_from…SimpleGraph.fromEdgeSet_edgeSet · cited by 2SimpleGraph.fromEdgeSet_e…SimpleGraph.fromEdgeSet_sdiff · cited by 2SimpleGraph.fromEdgeSet_s…Set · cited by 53352SetSimpleGraph · cited by 3072SimpleGraphSym2 · cited by 737Sym2Sym2.ToRel · cited by 9Sym2.ToRelSimpleGraph.fromEdgeSetCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • SimpleGraphstatement · cited by 3,072
  • Sym2statement and proof · cited by 737
  • Sym2.ToRelproof · cited by 9

Cited by46

Results whose statement or proof uses this declaration.