Lax Lean Archive

Refining a partition increases the flip metric

Lax185574.FlipMetricMonotone · concepts/Lax185574/FlipMetricMonotone.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

    Observation

    If 𝒬 refines 𝒫, then every 𝒫-flip is also a 𝒬-flip, and hence

    dist_𝒬(u, v) ≥ dist_𝒫(u, v).

    Concept map
    9 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 flipBall_subset_of_le proven

    2 isFlip_of_le proven

    In the paper

    • page 27 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Flips
    2
    3/-!
    4---
    5title: Refining a partition increases the flip metric
    6type: observation
    7---
    8If 𝒬 refines 𝒫, then every 𝒫-flip is also a 𝒬-flip, and hence
    9
    10dist_𝒬(u, v) ≥ dist_𝒫(u, v).
    11
    12# Formalization notes
    13
    14Refinement is 𝒬 ≤ 𝒫 for setoids. The inequality of the flip metrics is
    15stated through their balls: for every r, Ball^𝒬_r(v) ⊆ Ball^𝒫_r(v),
    16that is, dist_𝒬(u, v) ≤ r implies dist_𝒫(u, v) ≤ r. This is the
    17inequality for distances that may be infinite. The two parts of the
    18observation are two axioms. The graph may be infinite.
    19-/
    20
    21namespace Lax185574.FlipMetricMonotone
    22
    23open Lax185574.Flips
    24
    25universe u
    26
    27/-- If `𝒬` refines `𝒫`, every `𝒫`-flip is a `𝒬`-flip. -/
    28axiom isFlip_of_le {V : Type u} (G : SimpleGraph V) {P Q : Setoid V}
    29 (hQP : Q ≤ P) (H : SimpleGraph V) (hH : IsFlip G P H) : IsFlip G Q H
    30
    31/-- If `𝒬` refines `𝒫`, then `dist_𝒬(u, v) ≥ dist_𝒫(u, v)`: every ball
    32of the flip metric of `𝒬` lies in the ball of the same radius of the
    33flip metric of `𝒫`. -/
    34axiom flipBall_subset_of_le {V : Type u} (G : SimpleGraph V) {P Q : Setoid V}
    35 (hQP : Q ≤ P) (r : ℕ) (v : V) : flipBall G Q r v ⊆ flipBall G P r v
    36
    37end Lax185574.FlipMetricMonotone
    38
    Show ProofShow Proof
    Formalization notes

    Refinement is 𝒬 ≤ 𝒫 for setoids. The inequality of the flip metrics is stated through their balls: for every r, Ball^𝒬_r(v) ⊆ Ball^𝒫_r(v), that is, dist_𝒬(u, v) ≤ r implies dist_𝒫(u, v) ≤ r. This is the inequality for distances that may be infinite. The two parts of the observation are two axioms. The graph may be infinite.

    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…