Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-06 18:56 b3aa0524

View on Github →

feat(combinatorics/simple_graph/basic): introduce incidence sets, graph construction from relation (#5191) Add incidence sets and some lemmas, including a proof of equivalence between the neighbor set of a vertex and its incidence set. Add a graph construction from a given relation. Definitions and lemmas adapted from simple_graphs2

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.adj_incidence_set_inter

added theorem simple_graph.card_incidence_set_eq_degree

added theorem simple_graph.degree_pos_iff_exists_adj

added theorem simple_graph.edge_set_univ_card

added def simple_graph.from_rel

added theorem simple_graph.from_rel_adj

added def simple_graph.incidence_finset

added theorem simple_graph.incidence_other_neighbor_edge

added theorem simple_graph.incidence_other_prop

added def simple_graph.incidence_set

added def simple_graph.incidence_set_equiv_neighbor_set

added theorem simple_graph.incidence_set_subset

added def simple_graph.max_degree

added theorem simple_graph.mem_incidence_finset

added theorem simple_graph.mem_incidence_iff_neighbor

added theorem simple_graph.mem_incidence_set

added def simple_graph.min_degree

added def simple_graph.other_vertex_of_incident