Documentation

Complexity.Foundations.Data.OrderedSet

Optional minima of finite ordered sets #

The least-result contract includes absence: none means the eligible set is empty. It is independent of any tree, storage representation or cost model.

Main definitions #

Main results #

References #

Uses Mathlib's finite-set minimum and linear-order API.

source
def Cslib.OrderedSet.LeastResult {α : Type u_1} [LinearOrder α] (s : Finset α) :
Option α → Prop

A complete optional-minimum contract: none means no eligible key exists.

Instances For
    source
    def Cslib.OrderedSet.least {α : Type u_1} [LinearOrder α] (s : Finset α) :
    Option α

    The mathematical minimum, independent of any representation.

    Instances For
      source
      theorem Cslib.OrderedSet.least_spec {α : Type u_1} [LinearOrder α] (s : Finset α) :
      LeastResult s (least s)

      least s satisfies the optional-minimum contract for s.

      source
      theorem Cslib.OrderedSet.LeastResult.eq_least {α : Type u_1} [LinearOrder α] {s : Finset α} {a : Option α} (h : LeastResult s a) :
      a = least s

      Every result satisfying the optional-minimum contract for s is least s.

      source
      @[simp]
      theorem Cslib.OrderedSet.least_eq_min {α : Type u_1} [LinearOrder α] (s : Finset α) :
      least s = s.min

      least agrees with Finset.min (WithTop α is Option α).