Commit 2021-12-14 09:33 6d15ea43

View on Github →

feat(combinatorics/simple_graph): simp lemmas about spanning coe (#10778) A couple of lemmas from #8737 which don't involve connectivity, plus some extra related results. cc @kmill

Estimated changes

Modified src/combinatorics/simple_graph/subgraph.lean

added theorem simple_graph.subgraph.bot_adj_iff

added theorem simple_graph.subgraph.bot_verts

added theorem simple_graph.subgraph.map_spanning_top.injective

added def simple_graph.subgraph.map_spanning_top

added theorem simple_graph.subgraph.spanning_coe_top

added theorem simple_graph.subgraph.top_adj_iff

added theorem simple_graph.subgraph.top_verts

modified def simple_graph.to_subgraph