Theorems · Definition · combinatorics

SimpleGraph.IsIndContained

{V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Prop

A simple graph G is inducingly contained in a simple graph H if there exists an induced subgraph of H isomorphic to G. This is denoted by G ⊴ H.

Defined in

Mathlib.Combinatorics.SimpleGraph.Copy

Cited by

22 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms