Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Restricting an induced almost-embedding to its route union

Lax263307.HostRestriction · concepts/Lax263307/HostRestriction.lean · lax-263307

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

    Relabel the host graph induced by the nonempty union of edge routes onto Fin. The resulting graph embeds inducedly in the original host, has the same induced edge count, and supports the same induced almost-embedding with each route size preserved. Isolated source vertices may receive an arbitrary host image because they impose no endpoint condition.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.InducedRouteEdges
    2
    3/-!
    4---
    5title: Restricting an induced almost-embedding to its route union
    6type: theorem
    7---
    8Relabel the host graph induced by the nonempty union of edge routes onto
    9Fin. The resulting graph embeds inducedly in the original host, has the
    10same induced edge count, and supports the same induced almost-embedding
    11with each route size preserved. Isolated source vertices may receive an
    12arbitrary host image because they impose no endpoint condition.
    13
    14# Attribution
    15
    16The host restriction before applying the class width bound in Bonnet–Chang,
    17proof of Lemma 11.
    18-/
    19
    20namespace Lax263307.HostRestriction
    21
    22open Lax263307.AlmostEmbeddings Lax263307.InducedRouteEdges
    23
    24axiom restrict_to_route_union {t n : ℕ} (H : SimpleGraph (Fin t)) [DecidableRel H.Adj]
    25 (G : SimpleGraph (Fin n)) (E : AlmostEmbedding H G) (induced : IsInduced E)
    26 (nonempty : (routeUnion E).Nonempty) :
    27 ∃ r, ∃ K : SimpleGraph (Fin r), ∃ _f : K ↪g G, ∃ E' : AlmostEmbedding H K,
    28 IsInduced E' ∧ (∀ e, (E'.route e).card = (E.route e).card) ∧
    29 K.edgeSet.ncard = (G.induce (↑(routeUnion E) : Set (Fin n))).edgeSet.ncard
    30
    31end Lax263307.HostRestriction
    32
    Show Proof

    Attribution

    The host restriction before applying the class width bound in Bonnet–Chang, proof of Lemma 11.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…