Theorem SimpleGraph.disjoint_incidenceFinset_of_disjoint

Modification history

2026-09-05 14:32
Mathlib/Combinatorics/SimpleGraph/Finite.lean
feat(Combinatorics/SimpleGraph/Finite): the `Fintype` instance for `incidenceSet` doesn't need `DecidableEq` (#41713) …
Modified SimpleGraph.disjoint_incidenceFinset_of_disjointView on Github →
2026-07-20 03:19
Mathlib/Combinatorics/SimpleGraph/Finite.lean
feat(Combinatorics/SimpleGraph/Basic): `Disjoint` for graph sets (#41795)
Added SimpleGraph.disjoint_incidenceFinset_of_disjointView on Github →