Commit 2026-07-20 03:19 b300f2cc

View on Github →

feat(Combinatorics/SimpleGraph/Basic): Disjoint for graph sets (#41795)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.disjoint_commonNeighbors

added theorem SimpleGraph.disjoint_incidenceSet

added theorem SimpleGraph.disjoint_neighborSet

added theorem SimpleGraph.disjoint_of_disjoint_support

added theorem SimpleGraph.iUnion_incidenceSet

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.disjoint_incidenceFinset_of_disjoint

added theorem SimpleGraph.disjoint_neighborFinset_of_disjoint