Strict functional boundedness is a strict partial order
Lax825442.StrictlyBoundsOrder · concepts/Lax825442/StrictlyBoundsOrder.lean · lax-825442
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Strict functional boundedness is irreflexive and transitive on graph parameters, and hence is a strict partial order. The statement uses mathlib's , which expresses these two properties. Asymmetry follows from them. Distinct graph parameters can be functionally equivalent, so this is not asserted to be a strict total order.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax825442.StrictlyBounds |
| 2 | import Mathlib.Order.Defs.Unbundled |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Strict functional boundedness is a strict partial order |
| 7 | type: theorem |
| 8 | --- |
| 9 | Strict functional boundedness is irreflexive and transitive on graph |
| 10 | parameters, and hence is a strict partial order. The statement uses mathlib's |
| 11 | `IsStrictOrder`, which expresses these two properties. Asymmetry follows from |
| 12 | them. Distinct graph parameters can be functionally equivalent, so this is |
| 13 | not asserted to be a strict total order. |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax825442.StrictlyBoundsOrder |
| 17 | |
| 18 | open Lax153141.GraphParameters |
| 19 | |
| 20 | /-- Strict functional boundedness is an irreflexive, transitive relation. -/ |
| 21 | axiom strictlyBounds_strictOrder : |
| 22 | IsStrictOrder GraphParam Lax825442.StrictlyBounds.StrictlyBounds |
| 23 | |
| 24 | end Lax825442.StrictlyBoundsOrder |
| 25 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments