Lax Lean Archive

Invariance and characterization of graph crawling

Lax117614.GraphCrawlingInvariance · concepts/Lax117614/GraphCrawlingInvariance.lean · lax-117614

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

    Lemma

    Having a cheap crawl is invariant under isomorphism of website graphs, and a website graph is a yes-instance of the graph crawling problem exactly when it has a cheap crawl.

    Concept map
    9 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 graphCrawling_iff proven

    2 hasCheapCrawl_iso proven

    Lean source view on GitHub

    1import Lax904597.Classes
    2import Lax799700.Problems
    3import Lax117614.WebsiteGraphs
    4import Lax117614.GraphCrawlingProblem
    5
    6/-!
    7---
    8title: Invariance and characterization of graph crawling
    9type: lemma
    10---
    11Having a cheap crawl is invariant under isomorphism of website graphs, and
    12a website graph is a yes-instance of the graph crawling problem exactly
    13when it has a cheap crawl.
    14-/
    15
    16namespace Lax117614.GraphCrawlingInvariance
    17
    18open FirstOrder
    19
    20open FirstOrder.Language Structure
    21
    22open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    23open Lax117614.WebsiteGraphs Lax117614.GraphCrawlingProblem
    24
    25/-- The property `HasCheapCrawl` is isomorphism-invariant. -/
    26axiom hasCheapCrawl_iso : ∀ {A B : Type} [siteGraph.Structure A] [siteGraph.Structure B],
    27 (A ≃[siteGraph] B) → (HasCheapCrawl A ↔ HasCheapCrawl B)
    28
    29/-- The yes-instances of GraphCrawling are exactly the website graphs
    30satisfying `HasCheapCrawl`. -/
    31axiom graphCrawling_iff : ∀ (A : Type) [siteGraph.Structure A],
    32 GraphCrawling A ↔ HasCheapCrawl A
    33
    34end Lax117614.GraphCrawlingInvariance
    35
    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…