Commit 2024-02-03 03:33 620df7c2

View on Github →

refactor: split out finiteness properties for simple graphs (#10123)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree

deleted theorem SimpleGraph.DeleteFar.mono

deleted def SimpleGraph.DeleteFar

deleted theorem SimpleGraph.IsRegularOfDegree.compl

deleted theorem SimpleGraph.IsRegularOfDegree.degree_eq

deleted theorem SimpleGraph.IsRegularOfDegree.top

deleted def SimpleGraph.IsRegularOfDegree

deleted def SimpleGraph.LocallyFinite

deleted theorem SimpleGraph.bot_degree

deleted theorem SimpleGraph.card_commonNeighbors_le_degree_left

deleted theorem SimpleGraph.card_commonNeighbors_le_degree_right

deleted theorem SimpleGraph.card_commonNeighbors_lt_card_verts

deleted theorem SimpleGraph.card_commonNeighbors_top

deleted theorem SimpleGraph.card_edgeFinset_le_card_choose_two

deleted theorem SimpleGraph.card_edgeFinset_top_eq_card_choose_two

deleted theorem SimpleGraph.card_incidenceFinset_eq_degree

deleted theorem SimpleGraph.card_incidenceSet_eq_degree

deleted theorem SimpleGraph.card_neighborFinset_eq_degree

deleted theorem SimpleGraph.card_neighborSet_eq_degree

deleted theorem SimpleGraph.coe_edgeFinset

deleted theorem SimpleGraph.complete_graph_degree

deleted def SimpleGraph.degree

deleted theorem SimpleGraph.degree_compl

deleted theorem SimpleGraph.degree_le_maxDegree

deleted theorem SimpleGraph.degree_lt_card_verts

deleted theorem SimpleGraph.degree_pos_iff_exists_adj

deleted theorem SimpleGraph.deleteFar_iff

deleted def SimpleGraph.edgeFinset

deleted theorem SimpleGraph.edgeFinset_bot

deleted theorem SimpleGraph.edgeFinset_card

deleted theorem SimpleGraph.edgeFinset_deleteEdges

deleted theorem SimpleGraph.edgeFinset_inf

deleted theorem SimpleGraph.edgeFinset_inj

deleted theorem SimpleGraph.edgeFinset_sdiff

deleted theorem SimpleGraph.edgeFinset_ssubset_edgeFinset

deleted theorem SimpleGraph.edgeFinset_subset_edgeFinset

deleted theorem SimpleGraph.edgeFinset_sup

deleted theorem SimpleGraph.edgeFinset_top

deleted theorem SimpleGraph.edgeSet_univ_card

deleted theorem SimpleGraph.exists_maximal_degree_vertex

deleted theorem SimpleGraph.exists_minimal_degree_vertex

deleted def SimpleGraph.incidenceFinset

deleted theorem SimpleGraph.incidenceFinset_eq_filter

deleted theorem SimpleGraph.le_minDegree_of_forall_le_degree

deleted def SimpleGraph.maxDegree

deleted theorem SimpleGraph.maxDegree_le_of_forall_degree_le

deleted theorem SimpleGraph.maxDegree_lt_card_verts

deleted theorem SimpleGraph.mem_edgeFinset

deleted theorem SimpleGraph.mem_incidenceFinset

deleted theorem SimpleGraph.mem_neighborFinset

deleted def SimpleGraph.minDegree

deleted theorem SimpleGraph.minDegree_le_degree

deleted def SimpleGraph.neighborFinset

deleted theorem SimpleGraph.neighborFinset_compl

deleted theorem SimpleGraph.neighborFinset_def

deleted theorem SimpleGraph.neighborFinset_disjoint_singleton

deleted theorem SimpleGraph.neighborFinset_eq_filter

deleted theorem SimpleGraph.not_isDiag_of_mem_edgeFinset

deleted theorem SimpleGraph.not_mem_neighborFinset_self

deleted theorem SimpleGraph.singleton_disjoint_neighborFinset

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Created Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree

added theorem SimpleGraph.DeleteFar.mono

added def SimpleGraph.DeleteFar

added theorem SimpleGraph.IsRegularOfDegree.compl

added theorem SimpleGraph.IsRegularOfDegree.degree_eq

added theorem SimpleGraph.IsRegularOfDegree.top

added def SimpleGraph.IsRegularOfDegree

added def SimpleGraph.LocallyFinite

added theorem SimpleGraph.bot_degree

added theorem SimpleGraph.card_commonNeighbors_le_degree_left

added theorem SimpleGraph.card_commonNeighbors_le_degree_right

added theorem SimpleGraph.card_commonNeighbors_lt_card_verts

added theorem SimpleGraph.card_commonNeighbors_top

added theorem SimpleGraph.card_edgeFinset_le_card_choose_two

added theorem SimpleGraph.card_edgeFinset_top_eq_card_choose_two

added theorem SimpleGraph.card_incidenceFinset_eq_degree

added theorem SimpleGraph.card_incidenceSet_eq_degree

added theorem SimpleGraph.card_neighborFinset_eq_degree

added theorem SimpleGraph.card_neighborSet_eq_degree

added theorem SimpleGraph.coe_edgeFinset

added theorem SimpleGraph.complete_graph_degree

added def SimpleGraph.degree

added theorem SimpleGraph.degree_compl

added theorem SimpleGraph.degree_le_maxDegree

added theorem SimpleGraph.degree_lt_card_verts

added theorem SimpleGraph.degree_pos_iff_exists_adj

added theorem SimpleGraph.deleteFar_iff

added def SimpleGraph.edgeFinset

added theorem SimpleGraph.edgeFinset_bot

added theorem SimpleGraph.edgeFinset_card

added theorem SimpleGraph.edgeFinset_deleteEdges

added theorem SimpleGraph.edgeFinset_inf

added theorem SimpleGraph.edgeFinset_inj

added theorem SimpleGraph.edgeFinset_sdiff

added theorem SimpleGraph.edgeFinset_ssubset_edgeFinset

added theorem SimpleGraph.edgeFinset_subset_edgeFinset

added theorem SimpleGraph.edgeFinset_sup

added theorem SimpleGraph.edgeFinset_top

added theorem SimpleGraph.edgeSet_univ_card

added theorem SimpleGraph.exists_maximal_degree_vertex

added theorem SimpleGraph.exists_minimal_degree_vertex

added def SimpleGraph.incidenceFinset

added theorem SimpleGraph.incidenceFinset_eq_filter

added theorem SimpleGraph.le_minDegree_of_forall_le_degree

added def SimpleGraph.maxDegree

added theorem SimpleGraph.maxDegree_le_of_forall_degree_le

added theorem SimpleGraph.maxDegree_lt_card_verts

added theorem SimpleGraph.mem_edgeFinset

added theorem SimpleGraph.mem_incidenceFinset

added theorem SimpleGraph.mem_neighborFinset

added def SimpleGraph.minDegree

added theorem SimpleGraph.minDegree_le_degree

added def SimpleGraph.neighborFinset

added theorem SimpleGraph.neighborFinset_compl

added theorem SimpleGraph.neighborFinset_def

added theorem SimpleGraph.neighborFinset_disjoint_singleton

added theorem SimpleGraph.neighborFinset_eq_filter

added theorem SimpleGraph.not_isDiag_of_mem_edgeFinset

added theorem SimpleGraph.not_mem_neighborFinset_self

added theorem SimpleGraph.singleton_disjoint_neighborFinset

Modified Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified scripts/style-exceptions.txt