Lax Lean Archive

Splitting by minimal representatives preserves coarsening

Lax185574.SplittingMonotone Β· concepts/Lax185574/SplittingMonotone.lean Β· lax-185574

proven

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

    Lemma

    Fix a graph G together with a total order < on its vertices. Let 𝒫₁ β‰Ό 𝒫₂ β‰Ό β‹― β‰Ό 𝒫_m be a sequence of ever coarser partitions of V(G). Pick representatives T₁ βŠ‡ Tβ‚‚ βŠ‡ β‹― βŠ‡ T_m of 𝒫₁, …, 𝒫_m by setting

    T_i ≔ { min_<(P) : P ∈ 𝒫_i },

    and define 𝒬_i ≔ 𝒫_i ∧ T_i. Then 𝒬₁ β‰Ό 𝒬₂ β‰Ό β‹― β‰Ό 𝒬_m is also a sequence of ever coarser partitions.

    Concept map
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA β†’ B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 35 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeSplitting
    2
    3/-!
    4---
    5title: Splitting by minimal representatives preserves coarsening
    6type: lemma
    7---
    8Fix a graph G together with a total order < on its vertices. Let
    9𝒫₁ β‰Ό 𝒫₂ β‰Ό β‹― β‰Ό 𝒫_m be a sequence of ever coarser partitions of V(G). Pick
    10representatives T₁ βŠ‡ Tβ‚‚ βŠ‡ β‹― βŠ‡ T_m of 𝒫₁, …, 𝒫_m by setting
    11
    12T_i ≔ { min_<(P) : P ∈ 𝒫_i },
    13
    14and define 𝒬_i ≔ 𝒫_i ∧ T_i. Then 𝒬₁ β‰Ό 𝒬₂ β‰Ό β‹― β‰Ό 𝒬_m is also a sequence
    15of ever coarser partitions.
    16
    17# Formalization notes
    18
    19The paper uses this lemma inside the proof that the partitions of its
    20merge sequence get coarser.
    21
    22The order is a linear order on the vertex type. The set T_i is the set
    23of vertices that are minimal in their part, `minimalVertices`. On a
    24finite vertex type every part has a minimum, so this set is a
    25transversal. The conclusion needs no finiteness. The sequence is a
    26list, and the hypothesis and the conclusion compare consecutive
    27entries.
    28-/
    29
    30namespace Lax185574.SplittingMonotone
    31
    32open Lax185574.TypeSplitting
    33
    34universe z
    35
    36variable {V : Type z}
    37
    38/-- The vertices that are minimal in their part of `P`. -/
    39def minimalVertices [LinearOrder V] (P : Setoid V) : Set V :=
    40 {v | βˆ€ u : V, P u v β†’ v ≀ u}
    41
    42/-- **Coarsening is preserved.** Splitting ever coarser partitions
    43along their minimal vertices gives ever coarser partitions. -/
    44axiom split_minimalVertices_mono [LinearOrder V] (G : SimpleGraph V) (Ps : List (Setoid V))
    45 (h : βˆ€ (t : β„•) (ht : t + 1 < Ps.length), Ps[t] ≀ Ps[t + 1]) :
    46 βˆ€ (t : β„•) (ht : t + 1 < Ps.length),
    47 split G Ps[t] (minimalVertices Ps[t]) ≀ split G Ps[t + 1] (minimalVertices Ps[t + 1])
    48
    49end Lax185574.SplittingMonotone
    50
    Show Proof
    Formalization notes

    The paper uses this lemma inside the proof that the partitions of its merge sequence get coarser.

    The order is a linear order on the vertex type. The set T_i is the set of vertices that are minimal in their part, minimalVerticesminimalVertices. On a finite vertex type every part has a minimum, so this set is a transversal. The conclusion needs no finiteness. The sequence is a list, and the hypothesis and the conclusion compare consecutive entries.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…