Lax Lean Archive

Taking induced subgraphs and left lexicographic products

Lax871432.InducedSubgraphs · concepts/Lax871432/InducedSubgraphs.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 taking induced subgraphs,
    2. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under left lexicographic products,
    3. cl(F)\mathrm{cl}(\mathcal{F}) is closed under taking induced subgraphs,

    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 preservedUnderLeftLexProd_iff_cl_isInducedSubgraphClosed proven

    2 preservedUnderLeftLexProd_of_isInducedSubgraphClosed 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: Taking induced subgraphs and left lexicographic products
    8type: theorem
    9---
    10For a graph class F\mathcal{F} and the assertions
    11
    121. F\mathcal{F} is closed under taking induced subgraphs,
    132. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under left lexicographic products,
    143. cl(F)\mathrm{cl}(\mathcal{F}) is closed under taking induced subgraphs,
    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.InducedSubgraphs
    24
    25/-- **(1) ⇒\Rightarrow (2).** -/
    26axiom preservedUnderLeftLexProd_of_isInducedSubgraphClosed (𝓕 : GraphClass) :
    27 IsInducedSubgraphClosed 𝓕 → PreservedUnderLeftLexProd (homIndRel 𝓕)
    28
    29/-- **(2) ⇔\Leftrightarrow (3).** -/
    30axiom preservedUnderLeftLexProd_iff_cl_isInducedSubgraphClosed (𝓕 : GraphClass) :
    31 PreservedUnderLeftLexProd (homIndRel 𝓕) ↔ IsInducedSubgraphClosed (cl 𝓕)
    32
    33end Lax871432.InducedSubgraphs
    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…