Subtypes of conditionally complete linear orders #
In this file we give conditions on a subset of a conditionally complete linear order, to ensure that the subtype is itself conditionally complete.
We check that an OrdConnected
set satisfies these conditions.
TODO #
Add appropriate instances for all Set.Ixx
. This requires a refactor that will allow different
default values for supₛ
and infₛ
.
SupSet
structure on a nonempty subset s
of an object with SupSet
. This definition is
non-canonical (it uses default s
); it should be used only as here, as an auxiliary instance in the
construction of the ConditionallyCompleteLinearOrder
structure.
InfSet
structure on a nonempty subset s
of an object with InfSet
. This definition is
non-canonical (it uses default s
); it should be used only as here, as an auxiliary instance in the
construction of the ConditionallyCompleteLinearOrder
structure.
For a nonempty subset of a conditionally complete linear order to be a conditionally complete
linear order, it suffices that it contain the supₛ
of all its nonempty bounded-above subsets, and
the infₛ
of all its nonempty bounded-below subsets.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
The supₛ
function on a nonempty OrdConnected
set s
in a conditionally complete linear
order takes values within s
, for all nonempty bounded-above subsets of s
.
The infₛ
function on a nonempty OrdConnected
set s
in a conditionally complete linear
order takes values within s
, for all nonempty bounded-below subsets of s
.
A nonempty OrdConnected
set in a conditionally complete linear order is naturally a
conditionally complete linear order.
Equations
- One or more equations did not get rendered due to their size.