Lax Lean Archive

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

Functional equivalence of graph parameters

Lax825442.Equivalent · concepts/Lax825442/Equivalent.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

    Two graph parameters are functionally equivalent when each admits a functional bound in terms of the other. This does not require their numerical values to be equal, or either bounding function to be linear.

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

    Lean source view on GitHub

    1import Lax825442.Bounds
    2
    3/-!
    4---
    5title: Functional equivalence of graph parameters
    6type: definition
    7---
    8Two graph parameters are functionally equivalent when each admits a
    9functional bound in terms of the other. This does not require their numerical
    10values to be equal, or either bounding function to be linear.
    11-/
    12
    13namespace Lax825442.Equivalent
    14
    15open Lax153141.GraphParameters
    16
    17/-- Functional bounds hold in both directions. -/
    18def Equivalent (p q : GraphParam) : Prop :=
    19 (Lax825442.Bounds.Bounds p q) ∧ (Lax825442.Bounds.Bounds q p)
    20
    21end Lax825442.Equivalent
    22
    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…