Commit 2021-03-23 19:49 edfe7e1e

View on Github →

feat(combinatorics/simple_graph): degree lemmas (#5966) Proves some lemmas about the minimum/maximum degree of vertices in a graph - also weakens the assumptions for the definitions, following the usual mathlib pattern of defining total functions.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.degree_le_max_degree

added theorem simple_graph.exists_maximal_degree_vertex

added theorem simple_graph.exists_minimal_degree_vertex

added theorem simple_graph.le_min_degree_of_forall_le_degree

modified def simple_graph.max_degree

added theorem simple_graph.max_degree_le_of_forall_degree_le

added theorem simple_graph.max_degree_lt_card_verts

modified def simple_graph.min_degree

added theorem simple_graph.min_degree_le_degree