Given an order R on β and a function f : α → β, the preimage order on α is defined by x ≤ y ↔ f x ≤ f y. It is the unique order on α making f an order embedding (assuming f is injective).

A function between preorders is monotone if a ≤ b implies f a ≤ f b.

The pointwise partial order on a product. (The lexicographic ordering is defined in order/lexicographic.lean, and the instances are available via the type synonym lex α β = α × β.)

order without a top element; somtimes called cofinal

order without a bottom element; somtimes called coinitial or dense

An order is dense if there is an element between any pair of distinct elements.

Construct a partial order from a is_strict_order relation

This is basically the same as is_strict_total_order, but that definition is in Type (probably by mistake) and also has redundant assumptions.

Construct a linear order from a is_strict_total_order' relation

Construct a decidable linear order from a is_strict_total_order' relation

A connected order is one satisfying the condition a < c → a < b ∨ b < c. This is recognizable as an intuitionistic substitute for a ≤ b ∨ b ≤ a on the constructive reals, and is also known as negative transitivity, since the contrapositive asserts transitivity of the relation ¬ a < b.

An extensional relation is one in which an element is determined by its set of predecessors. It is named for the x ∈ y relation in set theory, whose extensionality is one of the first axioms of ZFC.

A well order is a well-founded linear order.

An unbounded or cofinal set

A bounded or final set

The minimum element of a nonempty set in a well-founded order

A family of elements of α is directed (with respect to a relation ≼ on α) if there is a member of the family ≼-above any pair in the family.

A subset of α is directed if there is an element of the set ≼-above any pair of elements in the set.

A monotone function on a linear order is directed.