Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-inf | 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 6939 | . 2 class inf(𝐴, 𝐵, 𝑅) |
5 | 3 | ccnv 4597 | . . 3 class ◡𝑅 |
6 | 1, 2, 5 | csup 6938 | . 2 class sup(𝐴, 𝐵, ◡𝑅) |
7 | 4, 6 | wceq 1342 | 1 wff inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) |
Colors of variables: wff set class |
This definition is referenced by: infeq1 6967 infeq2 6970 infeq3 6971 infeq123d 6972 nfinf 6973 eqinfti 6976 infvalti 6978 infclti 6979 inflbti 6980 infglbti 6981 infsnti 6986 inf00 6987 infisoti 6988 infex2g 6990 dfinfre 8842 infrenegsupex 9523 infxrnegsupex 11190 |
Copyright terms: Public domain | W3C validator |