Metamath Proof Explorer


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