Commit 2023-05-17 12:51 ce333e20

View on Github →

feat: port Combinatorics.SimpleGraph.Finsubgraph (#4010)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean

added def SimpleGraph.FinsubgraphHom.restrict

added def SimpleGraph.finsubgraphHomFunctor

added def SimpleGraph.finsubgraphOfAdj

added theorem SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom

added def SimpleGraph.singletonFinsubgraph

added theorem SimpleGraph.singletonFinsubgraph_le_adj_left

added theorem SimpleGraph.singletonFinsubgraph_le_adj_right