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 ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2		cR	⊢ 𝑅
3	0 1 2	cinf	⊢ inf ( 𝐴 , 𝐵 , 𝑅 )
4	2	ccnv	⊢ ◡ 𝑅
5	0 1 4	csup	⊢ sup ( 𝐴 , 𝐵 , ◡ 𝑅 )
6	3 5	wceq	⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 )