Lax Lean Archive

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

Absence of a functional bound

Lax825442.DoesNotBound · concepts/Lax825442/DoesNotBound.lean · lax-825442

definition

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

    Definition

    The relation p↛qp\not\to q says that there is no function bounding q(G)q(G) in terms of p(G)p(G) on all finite simple graphs. Requiring a bounding function to be nondecreasing does not change this notion: any natural-valued function can be replaced by its nondecreasing upper envelope.

    A graph family with uniformly bounded pp and unbounded qq witnesses this relation. An unknown catalogue entry does not assert this relation.

    Concept map
    3 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax825442.Bounds
    2
    3/-!
    4---
    5title: Absence of a functional bound
    6type: definition
    7---
    8The relation p↛qp\not\to q says that there is no function bounding q(G)q(G)
    9in terms of p(G)p(G) on all finite simple graphs. Requiring a bounding function
    10to be nondecreasing does not change this notion: any natural-valued function
    11can be replaced by its nondecreasing upper envelope.
    12
    13A graph family with uniformly bounded pp and unbounded qq witnesses this
    14relation. An unknown catalogue entry does not assert this relation.
    15-/
    16
    17namespace Lax825442.DoesNotBound
    18
    19open Lax153141.GraphParameters
    20
    21/-- No functional bound from `p` to `q` exists. -/
    22def DoesNotBound (p q : GraphParam) : Prop :=
    23 ¬ (Lax825442.Bounds.Bounds p q)
    24
    25end Lax825442.DoesNotBound
    26
    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…