| 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 9481 | . 2 class inf(𝐴, 𝐵, 𝑅) |
| 5 | 3 | ccnv 5684 | . . 3 class ◡𝑅 |
| 6 | 1, 2, 5 | csup 9480 | . 2 class sup(𝐴, 𝐵, ◡𝑅) |
| 7 | 4, 6 | wceq 1540 | 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
| Colors of variables: wff setvar class |
| This definition is referenced by: infeq1 9516 infeq2 9519 infeq3 9520 infeq123d 9521 nfinf 9522 infexd 9523 eqinf 9524 infval 9526 infcl 9528 inflb 9529 infglb 9530 infglbb 9531 fiinfcl 9541 infltoreq 9542 inf00 9546 infempty 9547 infiso 9548 dfinfre 12249 infrenegsup 12251 tosglb 32965 rencldnfilem 42831 |
| Copyright terms: Public domain | W3C validator |