Lax Lean Archive

Taking summands and preservation under disjoint unions

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

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

    2 preservedUnderDisjointUnion_of_isSummandClosed proven

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

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