Lax Lean Archive

Taking minors and preservation under complements

Lax871432.MinorsComplements · concepts/Lax871432/MinorsComplements.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 minor-closed,
    2. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under taking complements,
    3. cl(F)\mathrm{cl}(\mathcal{F}) is minor-closed,

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

    2 preservedUnderCompl_of_isMinorClosed proven

    In the paper

    • page 2 of this submission's paper
    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Lax871432.ClosureProperties
    2import Lax871432.DistinguishingClosure
    3import Lax871432.PreservationProperties
    4
    5/-!
    6---
    7title: Taking minors and preservation under complements
    8type: theorem
    9---
    10For a graph class F\mathcal{F} and the assertions
    11
    121. F\mathcal{F} is minor-closed,
    132. the relaxation ≡F\equiv_{\mathcal{F}} is preserved under taking complements,
    143. cl(F)\mathrm{cl}(\mathcal{F}) is minor-closed,
    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.MinorsComplements
    24
    25/-- **(1) ⇒\Rightarrow (2).** If `𝓕` is minor-closed then ≡F\equiv_{\mathcal{F}} is
    26preserved under taking complements. -/
    27axiom preservedUnderCompl_of_isMinorClosed (𝓕 : GraphClass) :
    28 IsMinorClosed 𝓕 → PreservedUnderCompl (homIndRel 𝓕)
    29
    30/-- **(2) ⇔\Leftrightarrow (3).** ≡F\equiv_{\mathcal{F}} is preserved under taking
    31complements if and only if cl(F)\mathrm{cl}(\mathcal{F}) is minor-closed. -/
    32axiom preservedUnderCompl_iff_cl_isMinorClosed (𝓕 : GraphClass) :
    33 PreservedUnderCompl (homIndRel 𝓕) ↔ IsMinorClosed (cl 𝓕)
    34
    35end Lax871432.MinorsComplements
    36
    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…