Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-30 06:52 864a43bc

View on Github →

feat(combinatorics/simple_graph): lemmas describing edge set of subgraphs (#11087)

Estimated changes

Modified src/combinatorics/simple_graph/subgraph.lean

added theorem disjoint.edge_set

added theorem simple_graph.subgraph.edge_set_bot

added theorem simple_graph.subgraph.edge_set_inf

added theorem simple_graph.subgraph.edge_set_mono

added theorem simple_graph.subgraph.edge_set_sup

added theorem simple_graph.subgraph.edge_set_top

added theorem simple_graph.subgraph.inf_adj

added theorem simple_graph.subgraph.spanning_coe_bot

added theorem simple_graph.subgraph.sup_adj