Theorems · Theorem · combinatorics

SimpleGraph.addCayley_le_iff

∀ {M : Type u_1} (s : Set M) [inst : Add M] (G : SimpleGraph M),
  SimpleGraph.addCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a + g ≠ a → G.Adj (a + g) a

Defined in

Mathlib.Combinatorics.SimpleGraph.Cayley

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

Add