mathlib3

da083dad - feat(combinatorics/simple_graph/hom): add basic definitions and lemmas for finite subgraphs (#16382)

feat(combinatorics/simple_graph/hom): add basic definitions and lemmas for finite subgraphs (#16382) We define `finsubgraph` and its corresponding vertex- and edge-based singletons, and prove some basic ordering lemmas on the singletons. This is primarily preparatory work for proving the De Bruijn-Erdős theorem (generalised to arbitrary finite codomain graphs). <!-- The text above the ` Co-authored-by: Kyle Miller <kmill31415@gmail.com>