Lax Lean Archive

Proof of `The pair relation grows under coarsening`

groundedproofs/Lax185574Proofs/PairRelationMonotone.lean · lax-185574

What this proof establishes

no assumptions

lem✓Lax185574.PairRelationMonotone

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 34 of this submission's paper

Description

On two copies of VV, the graph G[X,Y]G[X, Y] is a subgraph of G[X′,Y′]G[X', Y'] whenever X⊆X′X ⊆ X' and Y⊆Y′Y ⊆ Y', and likewise for Ḡ[X, Y]. The parts of 𝒫𝒫 lie in the parts of 𝒫′𝒫', so every short walk witnessing uv∈R(G,𝒫)uv ∈ R(G, 𝒫) is a walk in the graphs for 𝒫′𝒫'.