PR summary f7c1d6ebc9

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

I think this is reasonable, but just to check, what's the actual reason it's better to have this predicate and not just talk about emptiness of G.neighborSet v?

My reasoning is that there are many equivalent ways to write this condition (I can think of five that work in full generality), none of which seems particularly preferred, and I wanted to unify them all to a single new one for clarity and discoverability. It also happens to enable dot notation and correspond to a well-established informal notion

Makes sense, have you added the lemmas relating this to all five?

bors d+

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Here are the five seven I was thinking of, along with the lemmas proving they are equivalent to G.IsIsolated v:

• ∀ w, ¬ G.Adj v w, equational lemma for IsIsolated
• ∀ w, ¬ G.Adj w v, equational lemma for IsIsolated and adj_comm
• v ∉ G.support, mem_support_iff_not_isIsolated and not_not
• G.neighborSet v = ∅, neighborSet_eq_empty
• G.neighborFinset v = ∅, neighborFinset_eq_empty
• G.degree = 0, degree_eq_zero
• G.edegree = 0, missing because edegree doesn't exist yet

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style