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 8896
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 8894 . 2 class inf(𝐴, 𝐵, 𝑅)
53ccnv 5548 . . 3 class 𝑅
61, 2, 5csup 8893 . 2 class sup(𝐴, 𝐵, 𝑅)
74, 6wceq 1528 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  infeq1  8929  infeq2  8932  infeq3  8933  infeq123d  8934  nfinf  8935  infexd  8936  eqinf  8937  infval  8939  infcl  8941  inflb  8942  infglb  8943  infglbb  8944  fiinfcl  8954  infltoreq  8955  inf00  8959  infempty  8960  infiso  8961  dfinfre  11611  infrenegsup  11613  tosglb  30585  rencldnfilem  39297
  Copyright terms: Public domain W3C validator