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 8230 | . 2 class inf(𝐴, 𝐵, 𝑅) |
5 | 3 | ccnv 5037 | . . 3 class ◡𝑅 |
6 | 1, 2, 5 | csup 8229 | . 2 class sup(𝐴, 𝐵, ◡𝑅) |
7 | 4, 6 | wceq 1475 | 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
Colors of variables: wff setvar class |
This definition is referenced by: infeq1 8265 infeq2 8268 infeq3 8269 infeq123d 8270 nfinf 8271 infexd 8272 eqinf 8273 infval 8275 infcl 8277 inflb 8278 infglb 8279 infglbb 8280 fiinfcl 8290 infltoreq 8291 inf00 8294 infempty 8295 infiso 8296 lbinf 10855 dfinfre 10881 infrenegsup 10883 tosglb 29001 rencldnfilem 36402 |
Copyright terms: Public domain | W3C validator |