Order intervals #
This file defines (nonempty) closed intervals in an order (see
Set.Icc). This is a prototype for
Main declarations #
- fst : α
- snd : α
- fst_le_snd : s.fst ≤ s.snd
The starting point of an interval is smaller than the endpoint.
The nonempty closed intervals in an order.
Binary pushforward of nonempty intervals.