Lax Lean Archive

The pair relation grows under coarsening

Lax185574.PairRelationMonotone · concepts/Lax185574/PairRelationMonotone.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 and partitions 𝒫 and 𝒫′ of V(G) such that 𝒫 refines 𝒫′. Then R(G, 𝒫) ⊆ R(G, 𝒫′).

    Concept map
    10 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 34 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.PairRelation
    2
    3/-!
    4---
    5title: The pair relation grows under coarsening
    6type: lemma
    7---
    8Fix a graph G and partitions 𝒫 and 𝒫′ of V(G) such that 𝒫 refines 𝒫′.
    9Then R(G, 𝒫) ⊆ R(G, 𝒫′).
    10
    11# Formalization notes
    12
    13The relation R(G, 𝒫) is `PairRelation.pairRelation`, a simple graph,
    14and inclusion is the subgraph order. On two copies of V(G), the graph
    15G[X, Y] is a subgraph of G[X′, Y′] whenever X ⊆ X′ and Y ⊆ Y′, also
    16when X ≠ Y and X′ = Y′, and likewise for Ḡ[X, Y]. The proof in the
    17paper says more, that G[X, Y] is an induced subgraph of G[X′, Y′].
    18Distances only need the subgraph relation.
    19-/
    20
    21namespace Lax185574.PairRelationMonotone
    22
    23open Lax185574.PairRelation
    24
    25universe z
    26
    27/-- **Monotonicity of the pair relation.** Coarsening the partition can
    28only add pairs. -/
    29axiom pairRelation_mono {V : Type z} (G : SimpleGraph V) (P P' : Setoid V)
    30 (h : P ≤ P') : pairRelation G P ≤ pairRelation G P'
    31
    32end Lax185574.PairRelationMonotone
    33
    Show Proof
    Formalization notes

    The relation R(G, 𝒫) is PairRelation.pairRelationPairRelation.pairRelation, a simple graph, and inclusion is the subgraph order. On two copies of V(G), the graph G[X, Y] is a subgraph of G[X′, Y′] whenever X ⊆ X′ and Y ⊆ Y′, also when X ≠ Y and X′ = Y′, and likewise for Ḡ[X, Y]. The proof in the paper says more, that G[X, Y] is an induced subgraph of G[X′, Y′]. Distances only need the subgraph relation.

    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…