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 8899
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 8897 . 2 class inf(𝐴, 𝐵, 𝑅)
53ccnv 5552 . . 3 class 𝑅
61, 2, 5csup 8896 . 2 class sup(𝐴, 𝐵, 𝑅)
74, 6wceq 1530 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  infeq1  8932  infeq2  8935  infeq3  8936  infeq123d  8937  nfinf  8938  infexd  8939  eqinf  8940  infval  8942  infcl  8944  inflb  8945  infglb  8946  infglbb  8947  fiinfcl  8957  infltoreq  8958  inf00  8962  infempty  8963  infiso  8964  dfinfre  11614  infrenegsup  11616  tosglb  30571  rencldnfilem  39278
  Copyright terms: Public domain W3C validator