Definition df-inf

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	$$⊢sup\left(A,B,R\right)=sup\left(A,B,R^{-1}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2		cR	$$classR$$
3	0 1 2	cinf	$$classsup\left(A,B,R\right)$$
4	2	ccnv	$$class{R}^{-1}$$
5	0 1 4	csup	$$classsup\left(A,B,R^{-1}\right)$$
6	3 5	wceq	$$wffsup\left(A,B,R\right)=sup\left(A,B,R^{-1}\right)$$