Commit 2026-06-14 19:00 271d273e

View on Github →

feat(Combinatorics/SimpleGraph/Basic): more neighborSet and IsIsolated lemmas (#38747)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.Adj.nontrivial

added theorem SimpleGraph.Adj.not_isIsolated_left

added theorem SimpleGraph.Adj.not_isIsolated_right

added theorem SimpleGraph.IsIsolated.of_subsingleton

added theorem SimpleGraph.commonNeighbors_bot_eq

added theorem SimpleGraph.eq_bot_iff_isIsolated

added theorem SimpleGraph.exists_adj_iff_not_isIsolated

added theorem SimpleGraph.isIsolated_bot

added theorem SimpleGraph.neighborSet_bot

added theorem SimpleGraph.neighborSet_mono

added theorem SimpleGraph.neighborSet_ne_univ

added theorem SimpleGraph.neighborSet_subset_compl

added theorem SimpleGraph.neighborSet_top

added theorem SimpleGraph.nonempty_neighborSet

added theorem SimpleGraph.nontrivial_of_not_isIsolated

added theorem SimpleGraph.notMem_support_iff_isIsolated

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

deleted theorem SimpleGraph.neighborSet_mono

Modified Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean