Theorems · Theorem · combinatorics

Graph.restrict_isLink

∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) (e : β) (x y : α),
  (G.restrict E₀).IsLink e x y = (e ∈ E₀ ∧ G.IsLink e x y)

Defined in

Mathlib.Combinatorics.Graph.Delete

Cited by

3 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound