The monotone bijection between two sets of the same size #

A threshold in the unary representation of DescriptiveComplexity.Numbers.Unary is the size of a marked set, and “this set has exactly that size” is certified by a bijection with the marked set. A count of certificates needs the certificate to be unique, and a bijection is not: two sets of size k have k! of them. On a linearly ordered finite universe exactly one of them is monotone, and that is the one a counting kernel guesses.

DescriptiveComplexity.MonoBij K S F: the binary relation F is the graph of a monotone bijection from K onto S, as four first-order conditions;
DescriptiveComplexity.MonoBij.ncard_eq: such a graph makes the two sets the same size;
DescriptiveComplexity.exists_monoBij, DescriptiveComplexity.MonoBij.ext: on a finite linear order, two sets of the same size have one, and only one.

source

def DescriptiveComplexity.MonoBij {A : Type} [LE A] (K S : A → Prop) (F : A → A → Prop) :

Prop

The relation F is the graph of a monotone bijection from K onto S: it relates members of K to members of S, it is total on K and onto S, and it preserves and reflects the order. The last condition makes it functional and injective as well.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

source

theorem DescriptiveComplexity.MonoBij.functional {A : Type} [LinearOrder A] {K S : A → Prop} {F : A → A → Prop} (h : MonoBij K S F) {x y y' : A} (hy : F x y) (hy' : F x y') :

y = y'

A monotone bijection is functional.

Dependency graph

source

theorem DescriptiveComplexity.MonoBij.injective {A : Type} [LinearOrder A] {K S : A → Prop} {F : A → A → Prop} (h : MonoBij K S F) {x x' y : A} (hx : F x y) (hx' : F x' y) :

x = x'

A monotone bijection is injective.

Dependency graph

source