Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 03:33 db091637

View on Github →

feat(combinatorics/simple_graph/subgraph): single-vertex and single-edge subgraphs (#16435) Constructors for single-vertex and single-edge subgraphs along with some associated properties. Also includes dot notation improvements for simple_graph.subgraph.adj.

Estimated changes

Modified src/combinatorics/simple_graph/connectivity.lean

added def simple_graph.adj.to_walk

added theorem simple_graph.singleton_subgraph_connected

added theorem simple_graph.subgraph_of_adj_connected

Modified src/combinatorics/simple_graph/subgraph.lean

added theorem simple_graph.edge_set_singleton_subgraph

added theorem simple_graph.edge_set_subgraph_of_adj

added theorem simple_graph.eq_singleton_subgraph_iff_verts_eq

added theorem simple_graph.map_singleton_subgraph

added theorem simple_graph.map_subgraph_of_adj

added theorem simple_graph.neighbor_set_fst_subgraph_of_adj

added theorem simple_graph.neighbor_set_singleton_subgraph

added theorem simple_graph.neighbor_set_snd_subgraph_of_adj

added theorem simple_graph.neighbor_set_subgraph_of_adj

added theorem simple_graph.neighbor_set_subgraph_of_adj_of_ne_of_ne

added theorem simple_graph.neighbor_set_subgraph_of_adj_subset

added theorem simple_graph.singleton_subgraph_fst_le_subgraph_of_adj

added theorem simple_graph.singleton_subgraph_le_iff

added theorem simple_graph.singleton_subgraph_snd_le_subgraph_of_adj

added theorem simple_graph.subgraph.singleton_subgraph_eq_induce

added theorem simple_graph.subgraph.subgraph_of_adj_eq_induce

added def simple_graph.subgraph_of_adj

added theorem simple_graph.subgraph_of_adj_symm

Modified src/data/sym/sym2.lean

added theorem sym2.from_rel_bot

added theorem sym2.from_rel_top

Modified src/order/bounded_order.lean

added theorem Prop.bot_eq_false

added theorem Prop.top_eq_true