Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-17 02:13 b100af69

View on Github →

feat(combinatorics/simple_graph/basic): Incidence set lemmas (#10839) Some more simple_graph.incidence_set API.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.adj_iff_exists_edge_coe

added theorem simple_graph.adj_of_mem_incidence_set

modified theorem simple_graph.adj_symm

added theorem simple_graph.edge_mem_incidence_set_iff

added theorem simple_graph.incidence_set_inter_incidence_set

added theorem simple_graph.incidence_set_inter_incidence_set_subset

modified theorem simple_graph.incidence_set_subset

modified theorem simple_graph.mem_edge_set

added theorem simple_graph.mk_mem_incidence_set_iff

added theorem simple_graph.mk_mem_incidence_set_left_iff

added theorem simple_graph.mk_mem_incidence_set_right_iff

modified theorem simple_graph.ne_of_adj