Definition df-inf 6787

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 6785	. 2 class inf(𝐴, 𝐵, 𝑅)
5	3	ccnv 4476	. . 3 class ◡𝑅
6	1, 2, 5	csup 6784	. 2 class sup(𝐴, 𝐵, ◡𝑅)
7	4, 6	wceq 1299	1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅)

This definition is referenced by:  infeq1  6813  infeq2  6816  infeq3  6817  infeq123d  6818  nfinf  6819  eqinfti  6822  infvalti  6824  infclti  6825  inflbti  6826  infglbti  6827  infsnti  6832  inf00  6833  infisoti  6834  dfinfre  8572  infrenegsupex  9239  infxrnegsupex  10871