SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom

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

The theorem `SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom` states that for any types `V` and `W`, and any simple graphs `G` on `V` and `F` on `W` (where `F` is finite), if every finite subgraph `G'` of `G` has a homomorphism to `F`, then there exists a homomorphism from the entirety of `G` to `F`. In graph theory, a homomorphism from a graph `G` to a graph `F` is a function that maps vertices of `G` to vertices of `F` in such a way that adjacent vertices in `G` are mapped to adjacent vertices in `F`.

More concisely: If every finite subgraph of simple graph `G` has a homomorphism to finite graph `F`, then `G` has a homomorphism to `F`.