Conversation
sorrachai
reviewed
May 11, 2026
| Set.MapsTo f (components (deleteEdge G e)) | ||
| ((components G).disjSum {()}) ∧ | ||
| Set.InjOn f (components (deleteEdge G e)) := by | ||
| classical |
Collaborator
There was a problem hiding this comment.
Why this line is needed?
sorrachai
reviewed
May 11, 2026
|
|
||
| /-- The subgraph induced by a finite vertex set. -/ | ||
| @[simp, grind] noncomputable def inducedSubgraph (G : SimpleGraph α) (C : Finset α) : | ||
| SimpleGraph α := by classical |
sorrachai
reviewed
May 11, 2026
| /-! ## Induced subgraphs and component-wise counting identities -/ | ||
|
|
||
| /-- The subgraph induced by a finite vertex set. -/ | ||
| @[simp, grind] noncomputable def inducedSubgraph (G : SimpleGraph α) (C : Finset α) : |
Collaborator
There was a problem hiding this comment.
Can we avoid noncomputability? I want it to be computable by default.
sorrachai
reviewed
May 11, 2026
|
|
||
| /- `componentOf G v` is the connected component containing `v`. -/ | ||
| /-- The connected component containing `v`. -/ | ||
| @[simp, grind] noncomputable def componentOf (G : SimpleGraph α) (v : Vertex G) : Finset α := by |
Collaborator
There was a problem hiding this comment.
Can we avoid noncomputable?
sorrachai
reviewed
May 11, 2026
| Reachable G u v → Reachable H u v) | ||
| (hNum : numComponents G = numComponents H): | ||
| ∀ u v : α, | ||
| u ∈ G.vertexSet → v ∈ G.vertexSet → Reachable H u v → Reachable G u v := by classical |
Collaborator
There was a problem hiding this comment.
Suggested change
| u ∈ G.vertexSet → v ∈ G.vertexSet → Reachable H u v → Reachable G u v := by classical | |
| ∀ u ∈ V(G), ∀ v ∈ V(G), H.Reachable u v → G.Reachable u v := by classical |
Try to use notation more. My general comment is that try to make sure that the statement looks like English.
Collaborator
There was a problem hiding this comment.
This comment applies broadly
Collaborator
|
Does this relate to the previous merge? |
|
I may have a construction that could be relevant to this branch, on a different one I worked on and forgot to complete. On the file ParentTree.Basic I have the following: structure ParentTree (α : Type*) where
vertexSet : Finset α
parent : α -> α
level : α -> ℕ
incidence : ∀ v ∈ vertexSet, parent v ∈ vertexSet
ordering : ∀ v ∈ vertexSet, level v > 0 → level (parent v) < level v
root : ∀ v ∈ vertexSet, level v = 0 ↔ v = parent vLet me know if you want to coordinate so I can maybe merge those changes into this branch in case it fits |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add core graph-walk infrastructure and tree-related results for undirected simple graphs.
Split core walk definitions into
VertexSeqandWalkAdd helper lemmas for walk edge sets, vertex sequences, and walks in graphs
Add
deleteEdgefor simple graphsAdd component helper lemmas
Add bridge definitions and bridge-related lemmas
Add tree/forest definitions and tree's equivalence theorems