Lax Lean Archive

Splitting the parts of a partition by atomic types over a set

Lax185574.TypeSplitting · concepts/Lax185574/TypeSplitting.lean · lax-185574

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

    Fix a graph G and a partition 𝒫 of V(G). For a set T ⊆ V(G), 𝒫 ∧ T is the refinement of 𝒫 where each part P ∈ 𝒫 is split into atomic types over T ∖ P, that is, into sets of the form P ∩ Q, where Q is the set of all vertices of G with a given neighborhood in T ∖ P.

    Concept map
    7 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 32 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Partitions
    2
    3/-!
    4---
    5title: Splitting the parts of a partition by atomic types over a set
    6type: definition
    7---
    8Fix a graph G and a partition 𝒫 of V(G). For a set T ⊆ V(G), 𝒫 ∧ T is
    9the refinement of 𝒫 where each part P ∈ 𝒫 is split into atomic types
    10over T ∖ P, that is, into sets of the form P ∩ Q, where Q is the set of
    11all vertices of G with a given neighborhood in T ∖ P.
    12
    13# Formalization notes
    14
    15The partition 𝒫 ∧ T is the kernel of the map sending v to its part
    16𝒫(v) together with N(v) ∩ (T ∖ 𝒫(v)). Two vertices have the same image
    17exactly when they lie in the same part P and have the same neighborhood
    18in T ∖ P, which is the description of the paper. A vertex of P does not
    19lie in T ∖ P, so its atomic type over T ∖ P is given by this
    20neighborhood alone. If 𝒫 has a single part, then T ∖ P is empty and
    21𝒫 ∧ T = 𝒫.
    22-/
    23
    24namespace Lax185574.TypeSplitting
    25
    26universe z
    27
    28variable {V : Type z}
    29
    30/-- `𝒫 ∧ T`: each part `P` of `P` is split according to the
    31neighborhoods of its vertices in `T ∖ P`. -/
    32def split (G : SimpleGraph V) (P : Setoid V) (T : Set V) : Setoid V :=
    33 Setoid.ker fun v => (Quotient.mk P v, {t | t ∈ T ∧ ¬ P t v} ∩ G.neighborSet v)
    34
    35end Lax185574.TypeSplitting
    36
    Formalization notes

    The partition 𝒫 ∧ T is the kernel of the map sending v to its part 𝒫(v) together with N(v) ∩ (T ∖ 𝒫(v)). Two vertices have the same image exactly when they lie in the same part P and have the same neighborhood in T ∖ P, which is the description of the paper. A vertex of P does not lie in T ∖ P, so its atomic type over T ∖ P is given by this neighborhood alone. If 𝒫 has a single part, then T ∖ P is empty and 𝒫 ∧ T = 𝒫.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…