Syntax Definition cinf 9130

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

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cR	class 𝑅

Assertion

Ref	Expression
cinf	class inf(𝐴, 𝐵, 𝑅)

See definition df-inf 9132 for more information.