Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-inf | Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cR | . . 3 | |
4 | 1, 2, 3 | cinf 6870 | . 2 inf |
5 | 3 | ccnv 4538 | . . 3 |
6 | 1, 2, 5 | csup 6869 | . 2 |
7 | 4, 6 | wceq 1331 | 1 inf |
Colors of variables: wff set class |
This definition is referenced by: infeq1 6898 infeq2 6901 infeq3 6902 infeq123d 6903 nfinf 6904 eqinfti 6907 infvalti 6909 infclti 6910 inflbti 6911 infglbti 6912 infsnti 6917 inf00 6918 infisoti 6919 dfinfre 8714 infrenegsupex 9389 infxrnegsupex 11032 |
Copyright terms: Public domain | W3C validator |