Description: Define the infimum of class A . It is meaningful when R is a relation that strictly orders B and when the infimum exists. For example, R could be 'less than', B could be the set of real numbers, and A could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-inf | |- inf ( A , B , R ) = sup ( A , B , `' R ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | |- A |
|
1 | cB | |- B |
|
2 | cR | |- R |
|
3 | 0 1 2 | cinf | |- inf ( A , B , R ) |
4 | 2 | ccnv | |- `' R |
5 | 0 1 4 | csup | |- sup ( A , B , `' R ) |
6 | 3 5 | wceq | |- inf ( A , B , R ) = sup ( A , B , `' R ) |