Definition df-inf 6398

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.)

Assertion

Ref	Expression
df-inf	|- inf ( A , B , R ) = sup ( A , B , `' R )

Detailed syntax breakdown of Definition df-inf

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4	1, 2, 3	cinf 6396	. 2 class inf ( A , B , R )
5	3	ccnv 4362	. . 3 class `' R
6	1, 2, 5	csup 6395	. 2 class sup ( A , B , `' R )
7	4, 6	wceq 1284	1 wff inf ( A , B , R ) = sup ( A , B , `' R )

This definition is referenced by:  infeq1  6424  infeq2  6427  infeq3  6428  infeq123d  6429  nfinf  6430  eqinfti  6433  infvalti  6435  infclti  6436  inflbti  6437  infglbti  6438  infsnti  6443  inf00  6444  infisoti  6445  dfinfre  8034  infrenegsupex  8682