Lax Lean Archive

Lax14.OrderTypes

Order type of a tuple

concepts/Lax14/OrderTypes.lean · lax-14

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    Fix a linearly ordered set and a tuple a = (a₁, …, a_ℓ) of its elements. The order type of a records which coordinates carry strictly smaller entries than which: it is the relation that holds of i and j when aᵢ < aⱼ. Two tuples have the same order type when they are arranged in the same way — in particular they then agree on which coordinates carry equal entries, since a linear order is total.

    Lean source view on GitHub

    1import Mathlib.Order.Basic
    2import Mathlib.Data.Fin.Basic
    3
    4/-!
    5---
    6title: Order type of a tuple
    7type: definition
    8---
    9Fix a linearly ordered set and a tuple *a* = (*a*₁, …, *a*_ℓ) of its
    10elements. The order type of *a* records which coordinates carry strictly
    11smaller entries than which: it is the relation that holds of *i* and *j*
    12when *a*ᵢ < *a*ⱼ. Two tuples have the same order type when they are
    13arranged in the same way — in particular they then agree on which
    14coordinates carry equal entries, since a linear order is total.
    15
    16# Formalization notes
    17
    18The order type is a `Prop`-valued relation on coordinates rather than a
    19three-valued code: in a linear order the strict-order pattern determines
    20the equality pattern (`a i = a j` exactly when neither `a i < a j` nor
    21`a j < a i`), so recording `<` alone loses nothing and keeps
    22decidability, `compare` and `Ordering` off the endorsement surface.
    23
    24The definition is stated for an arbitrary linearly ordered vertex type,
    25not only for `Fin n`: it is a pointwise notion, and proofs that consume it
    26work over intermediate carriers. Statements of this submission still
    27instantiate it at the canonical carriers.
    28-/
    29
    30namespace Lax14.OrderTypes
    31
    32/-- The order type of a tuple: the relation holding of coordinates `i` and
    33`j` when the `i`-th entry is strictly smaller than the `j`-th. Two tuples
    34have the same order type when this relation is the same. -/
    35def orderType {V : Type*} [LinearOrder V] {ℓ : ℕ} (a : Fin ℓ → V) :
    36 Fin ℓ → Fin ℓ → Prop :=
    37 fun i j => a i < a j
    38
    39end Lax14.OrderTypes
    40

    Formalization notes

    The order type is a PropProp-valued relation on coordinates rather than a three-valued code: in a linear order the strict-order pattern determines the equality pattern (ai=aja i = a j exactly when neither ai<aja i < a j nor aj<aia j < a i), so recording << alone loses nothing and keeps decidability, comparecompare and OrderingOrdering off the endorsement surface.

    The definition is stated for an arbitrary linearly ordered vertex type, not only for FinnFin n: it is a pointwise notion, and proofs that consume it work over intermediate carriers. Statements of this submission still instantiate it at the canonical carriers.

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…