Commit 2026-01-24 00:25 038dd597

View on Github →

refactor(SimpleGraph/Finite): turn edgeFinset into a def (#28821) Also add some API lemmas.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.Adj.degree_pos_left

added theorem SimpleGraph.Adj.degree_pos_right

added theorem SimpleGraph.card_edgeSet

added theorem SimpleGraph.coe_incidenceFinset

added theorem SimpleGraph.coe_neighborFinset

added theorem SimpleGraph.degree_pos_iff_nonempty

added def SimpleGraph.edgeFinset

modified theorem SimpleGraph.edgeFinset_inj

modified theorem SimpleGraph.edgeFinset_ssubset_edgeFinset

modified theorem SimpleGraph.edgeFinset_subset_edgeFinset

modified theorem SimpleGraph.edgeSet_univ_card

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean