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	|- inf ( A , B , R ) = sup ( A , B , `' R )

Detailed syntax breakdown

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 )