Lax Lean Archive

Contracting edges and right lexicographic products

Lax871432.EdgeContractions · concepts/Lax871432/EdgeContractions.lean · lax-871432

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

    Theorem

    For a graph class F\mathcal{F} and the assertions

    1. F\mathcal{F} is closed under contracting edges,
    2. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under right lexicographic products,
    3. cl(F)\mathrm{cl}(\mathcal{F}) is closed under contracting edges,

    the implications (1) ⇒\Rightarrow (2) ⇔\Leftrightarrow (3) hold.

    Concept map
    11 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 preservedUnderRightLexProd_iff_cl_isContractionClosed proven

    2 preservedUnderRightLexProd_of_isContractionClosed proven

    In the paper

    • page 10 of this submission's paper

    Lean source view on GitHub

    1import Lax871432.ClosureProperties
    2import Lax871432.DistinguishingClosure
    3import Lax871432.PreservationProperties
    4
    5/-!
    6---
    7title: Contracting edges and right lexicographic products
    8type: theorem
    9---
    10For a graph class F\mathcal{F} and the assertions
    11
    121. F\mathcal{F} is closed under contracting edges,
    132. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under right lexicographic products,
    143. cl(F)\mathrm{cl}(\mathcal{F}) is closed under contracting edges,
    15
    16the implications (1) ⇒\Rightarrow (2) ⇔\Leftrightarrow (3) hold.
    17-/
    18
    19open Lax871432.ClosureProperties Lax871432.DistinguishingClosure
    20open Lax871432.GraphClasses
    21open Lax871432.HomomorphismIndistinguishability Lax871432.PreservationProperties
    22
    23namespace Lax871432.EdgeContractions
    24
    25/-- **(1) ⇒\Rightarrow (2).** -/
    26axiom preservedUnderRightLexProd_of_isContractionClosed (𝓕 : GraphClass) :
    27 IsContractionClosed 𝓕 → PreservedUnderRightLexProd (homIndRel 𝓕)
    28
    29/-- **(2) ⇔\Leftrightarrow (3).** -/
    30axiom preservedUnderRightLexProd_iff_cl_isContractionClosed (𝓕 : GraphClass) :
    31 PreservedUnderRightLexProd (homIndRel 𝓕) ↔ IsContractionClosed (cl 𝓕)
    32
    33end Lax871432.EdgeContractions
    34
    Show ProofShow Proof
    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…