MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-inf Structured version   Visualization version   GIF version

Definition df-inf 8334
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3cinf 8332 . 2 class inf(𝐴, 𝐵, 𝑅)
53ccnv 5103 . . 3 class 𝑅
61, 2, 5csup 8331 . 2 class sup(𝐴, 𝐵, 𝑅)
74, 6wceq 1481 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  infeq1  8367  infeq2  8370  infeq3  8371  infeq123d  8372  nfinf  8373  infexd  8374  eqinf  8375  infval  8377  infcl  8379  inflb  8380  infglb  8381  infglbb  8382  fiinfcl  8392  infltoreq  8393  inf00  8396  infempty  8397  infiso  8398  lbinf  10961  dfinfre  10989  infrenegsup  10991  tosglb  29644  rencldnfilem  37203
  Copyright terms: Public domain W3C validator