Lax Lean Archive

Transitivity of definable flips

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

    Fact

    Let G₁ be an s₁-definable flip of G₀ and G₂ be an s₂-definable flip of G₁. Then G₂ is an (s₁ + s₂)-definable flip of G₀.

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

    Lean source view on GitHub

    1import Lax185574.DefinableFlips
    2
    3/-!
    4---
    5title: Transitivity of definable flips
    6type: fact
    7---
    8Let G₁ be an s₁-definable flip of G₀ and G₂ be an s₂-definable flip of
    9G₁. Then G₂ is an (s₁ + s₂)-definable flip of G₀.
    10
    11# Formalization notes
    12
    13The three graphs share a vertex type, which may be infinite. The paper
    14states this as well known and refers to Lemma 2.6 in the full version
    15of the cited work on flipper games. With the definition of
    16`DefinableFlips`, the parameter set of G₂ over G₀ can be taken to be the
    17union of the two given parameter sets.
    18-/
    19
    20namespace Lax185574.DefinableFlipTransitivity
    21
    22open Lax185574.DefinableFlips
    23
    24universe u
    25
    26/-- **Transitivity of definable flips.** An `s₂`-definable flip of an
    27`s₁`-definable flip of `G₀` is an `(s₁ + s₂)`-definable flip of `G₀`. -/
    28axiom isDefinableFlip_trans {V : Type u} {G₀ G₁ G₂ : SimpleGraph V}
    29 {s₁ s₂ : ℕ} (h₁ : IsDefinableFlip G₀ s₁ G₁) (h₂ : IsDefinableFlip G₁ s₂ G₂) :
    30 IsDefinableFlip G₀ (s₁ + s₂) G₂
    31
    32end Lax185574.DefinableFlipTransitivity
    33
    Show Proof
    Formalization notes

    The three graphs share a vertex type, which may be infinite. The paper states this as well known and refers to Lemma 2.6 in the full version of the cited work on flipper games. With the definition of DefinableFlipsDefinableFlips, the parameter set of G₂ over G₀ can be taken to be the union of the two given parameter sets.

    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…