Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-24 23:25 d4d33dea

View on Github →

feat(combinatorics): define simple graphs (#3458) adds basic definition of simple_graphs

Estimated changes

added def complete_graph
added theorem simple_graph.edge_symm
added theorem simple_graph.irrefl
added theorem simple_graph.ne_of_adj
added structure simple_graph
added theorem sym2.elems_iff_eq
modified theorem sym2.mem_iff
added theorem sym2.mk_has_mem_right
modified inductive sym2.rel
added def sym2.rel_bool
added theorem sym2.rel_bool_spec
modified def sym2