Theorems · Inductive type · order theory

Order.Cofinal

(P : Type u_2) → [Preorder P] → Type u_2

For a preorder P, Cofinal P is the type of subsets of P containing arbitrarily large elements. They are the dense sets in the topology whose open sets are terminal segments.

Defined in

Mathlib.Order.Ideal

Cited by

13 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Preorder