Syntax Definition cinf 8347

Description: Extend class notation to include infimum of class A. Here R is ordinarily a relation that strictly orders class B. For example, R could be 'less than' and B could be the set of real numbers.

Hypotheses

Ref	Expression
cA	class A
cB	class B
cR	class R

Assertion

Ref	Expression
cinf	class inf ( A , B , R )

See definition df-inf 8349 for more information.