Strict functional boundedness of graph parameters
Lax825442.StrictlyBounds · concepts/Lax825442/StrictlyBounds.lean · lax-825442
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A graph parameter p strictly bounds q when q is bounded by a nondecreasing function of p on all finite simple graphs, but p admits no functional bound in terms of q. This does not assert a pointwise strict inequality between their values. It is the strict part of functional boundedness.
Concept map
Lean source view on GitHub
| 1 | import Lax825442.DoesNotBound |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Strict functional boundedness of graph parameters |
| 6 | type: definition |
| 7 | --- |
| 8 | A graph parameter p strictly bounds q when q is bounded by a nondecreasing |
| 9 | function of p on all finite simple graphs, but p admits no functional bound |
| 10 | in terms of q. This does not assert a pointwise strict inequality between |
| 11 | their values. It is the strict part of functional boundedness. |
| 12 | -/ |
| 13 | |
| 14 | namespace Lax825442.StrictlyBounds |
| 15 | |
| 16 | open Lax153141.GraphParameters |
| 17 | |
| 18 | /-- Functional boundedness holds in one direction and fails in the reverse. -/ |
| 19 | def StrictlyBounds (p q : GraphParam) : Prop := |
| 20 | (Lax825442.Bounds.Bounds p q) ∧ |
| 21 | (Lax825442.DoesNotBound.DoesNotBound q p) |
| 22 | |
| 23 | end Lax825442.StrictlyBounds |
| 24 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments