![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-inf | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-inf | ⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cR | . . 3 class 𝑅 | |
4 | 1, 2, 3 | cinf 9478 | . 2 class inf(𝐴, 𝐵, 𝑅) |
5 | 3 | ccnv 5687 | . . 3 class ◡𝑅 |
6 | 1, 2, 5 | csup 9477 | . 2 class sup(𝐴, 𝐵, ◡𝑅) |
7 | 4, 6 | wceq 1536 | 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
Colors of variables: wff setvar class |
This definition is referenced by: infeq1 9513 infeq2 9516 infeq3 9517 infeq123d 9518 nfinf 9519 infexd 9520 eqinf 9521 infval 9523 infcl 9525 inflb 9526 infglb 9527 infglbb 9528 fiinfcl 9538 infltoreq 9539 inf00 9543 infempty 9544 infiso 9545 dfinfre 12246 infrenegsup 12248 tosglb 32949 rencldnfilem 42807 |
Copyright terms: Public domain | W3C validator |