Definition df-inf 6457

Description: Define the infimum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the infimum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 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(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

Detailed syntax breakdown of Definition df-inf

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4	1, 2, 3	cinf 6455	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 4370	. . 3 class ◡𝑅
6	1, 2, 5	csup 6454	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1285	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  6483  infeq2  6486  infeq3  6487  infeq123d  6488  nfinf  6489  eqinfti  6492  infvalti  6494  infclti  6495  inflbti  6496  infglbti  6497  infsnti  6502  inf00  6503  infisoti  6504  dfinfre  8101  infrenegsupex  8763