Theorems · Theorem · combinatorics

SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom

∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {F : SimpleGraph W} [Finite W]
  (h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F), Nonempty (G →g F)

If every finite subgraph of a graph G has a homomorphism to a finite graph F, then there is a homomorphism from the whole of G to F.

Defined in

Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite