Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The components left by deleting a separator

Lax263307.SeparatorComponents · concepts/Lax263307/SeparatorComponents.lean · lax-263307

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Deleting a vertex set SS partitions the remaining vertices into connected components. Every undeleted vertex belongs to exactly one part, and every edge with undeleted endpoints has both endpoints in one part. These are the properties used to combine the recursive independent sets.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Lax263307.LinearRelaxation
    2import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    3
    4/-!
    5---
    6title: The components left by deleting a separator
    7type: definition
    8---
    9Deleting a vertex set SS partitions the remaining vertices into connected
    10components. Every undeleted vertex belongs to exactly one part, and every
    11edge with undeleted endpoints has both endpoints in one part. These are the
    12properties used to combine the recursive independent sets.
    13
    14# Formalization notes
    15
    16`Partition` also permits grouping connected components together. The canonical
    17`components` construction uses precisely the connected components of G−SG-S.
    18The vertex sets of the parts are finite sets in the original vertex type.
    19-/
    20
    21namespace Lax263307.SeparatorComponents
    22
    23/-- A partition of the undeleted vertices, closed under undeleted edges. -/
    24structure Partition {n : ℕ} (G : SimpleGraph (Fin n))
    25 (S : Finset (Fin n)) (ι : Type) where
    26 /-- The original vertices in each part. -/
    27 vertices : ι → Finset (Fin n)
    28 /-- Parts exclude the deleted vertices. -/
    29 outside : ∀ i v, v ∈ vertices i → v ∉ S
    30 /-- Every undeleted vertex belongs to exactly one part. -/
    31 unique : ∀ v, v ∉ S → ∃! i, v ∈ vertices i
    32 /-- No undeleted edge leaves a part. -/
    33 closed : ∀ i u v, u ∈ vertices i → v ∉ S → G.Adj u v → v ∈ vertices i
    34
    35/-- Connected components of the induced graph give the canonical partition. -/
    36noncomputable def components {n : ℕ} (G : SimpleGraph (Fin n))
    37 (S : Finset (Fin n)) :
    38 Partition G S (G.induce (↑S : Set (Fin n))ᶜ).ConnectedComponent := by
    39 classical
    40 let H := G.induce (↑S : Set (Fin n))ᶜ
    41 let vertices (c : H.ConnectedComponent) := (Subtype.val '' c.supp).toFinset
    42 exact
    43 { vertices := vertices
    44 outside := by
    45 intro c v hv
    46 obtain ⟨u, _, rfl⟩ := Set.mem_toFinset.mp hv
    47 exact u.property
    48 unique := by
    49 intro v hv
    50 let u : ↥((↑S : Set (Fin n))ᶜ) := ⟨v, hv⟩
    51 refine ⟨H.connectedComponentMk u, ?_, ?_⟩
    52 · exact Set.mem_toFinset.mpr ⟨u, rfl, rfl⟩
    53 · intro c hc
    54 obtain ⟨w, hw, he⟩ := Set.mem_toFinset.mp hc
    55 have hwu : w = u := Subtype.ext he
    56 change H.connectedComponentMk w = c at hw
    57 rw [hwu] at hw
    58 exact hw.symm
    59 closed := by
    60 intro c u v hu hv huv
    61 obtain ⟨u', hu', rfl⟩ := Set.mem_toFinset.mp hu
    62 let v' : ↥((↑S : Set (Fin n))ᶜ) := ⟨v, hv⟩
    63 exact Set.mem_toFinset.mpr ⟨v',
    64 (SimpleGraph.ConnectedComponent.mem_supp_congr_adj c
    65 (show H.Adj u' v' from huv)).mp hu', rfl⟩ }
    66
    67/-- The recursive answer is the union of the answers on the parts. -/
    68def combine {n : ℕ} {ι : Type} [Fintype ι] (I : ι → Finset (Fin n)) :
    69 Finset (Fin n) := Finset.univ.biUnion I
    70
    71end Lax263307.SeparatorComponents
    72
    Formalization notes

    PartitionPartition also permits grouping connected components together. The canonical componentscomponents construction uses precisely the connected components of G−SG-S. The vertex sets of the parts are finite sets in the original vertex type.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…