This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Define the infimum of class A . It is meaningful when R is a relation that strictly orders B and when the infimum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 | ||
|---|---|---|---|
| Assertion | df-inf | ⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | cB | ⊢ 𝐵 | |
| 2 | cR | ⊢ 𝑅 | |
| 3 | 0 1 2 | cinf | ⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) |
| 4 | 2 | ccnv | ⊢ ◡ 𝑅 |
| 5 | 0 1 4 | csup | ⊢ sup ( 𝐴 , 𝐵 , ◡ 𝑅 ) |
| 6 | 3 5 | wceq | ⊢ inf ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , ◡ 𝑅 ) |