The image under a monotone function of a set which is bounded above is bounded above
The image under a monotone function of a set which is bounded below is bounded below
When there is a global maximum, every set is bounded above.
When there is a global minimum, every set is bounded below.
The union of two sets is bounded above if and only if each of the sets is.
Adding a point to a set preserves its boundedness above.
A finite set is bounded above.
A finite union of sets which are all bounded above is still bounded above.
The union of two sets is bounded below if and only if each of the sets is.
Adding a point to a set preserves its boundedness below.
A finite set is bounded below.
A finite union of sets which are all bounded below is still bounded below.
A conditionally complete lattice is a lattice in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers.
To differentiate the statements from the corresponding statements in (unconditional) complete lattices, we prefix Inf and Sup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of non-emptyness or boundedness.
Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w<b.
Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w>b.
When an element a of a set s is larger than all elements of the set, it is Sup s
When an element a of a set s is smaller than all elements of the set, it is Inf s
b < Sup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptyness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.
Inf s < b s when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptyness and linear order for the other one), so we formulate separately the two implications, contrary to the complete_lattice case.
The supremum of a singleton is the element of the singleton
The infimum of a singleton is the element of the singleton
If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.
The sup of a union of sets is the max of the suprema of each subset, under the assumptions that all sets are bounded above and nonempty.
The inf of a union of sets is the min of the infima of each subset, under the assumptions that all sets are bounded below and nonempty.
The supremum of an intersection of sets is bounded by the minimum of the suprema of each set, if all sets are bounded above and nonempty.
The infimum of an intersection of sets is bounded below by the maximum of the infima of each set, if all sets are bounded below and nonempty.
The supremum of insert a s is the maximum of a and the supremum of s, if s is nonempty and bounded above.
The infimum of insert a s is the minimum of a and the infimum of s, if s is nonempty and bounded below.
The indexed supremum of two functions are comparable if the functions are pointwise comparable
The indexed supremum of a function is bounded above by a uniform bound
The indexed supremum of a function is bounded below by the value taken at one point
The indexed infimum of two functions are comparable if the functions are pointwise comparable
The indexed minimum of a function is bounded below by a uniform lower bound
The indexed infimum of a function is bounded above by the value taken at one point
When b < Sup s, there is an element a in s with b < a, if s is nonempty and the order is a linear order.
Indexed version of the above lemma exists_lt_of_lt_cSup. When b < supr f, there is an element i such that b < f i.
When Inf s < b, there is an element a in s with a < b, if s is nonempty and the order is a linear order.
Indexed version of the above lemma exists_lt_of_cInf_lt When infi f < a, there is an element i such that f i < a.
Introduction rule to prove that b is the supremum of s: it suffices to check that
This instance is necessary, otherwise the lattice operations would be derived via conditionally_complete_linear_order_bot and marked as noncomputable.