Metamath Proof Explorer


Syntax definition ccref

Description: The "every open cover has an A refinement" predicate.

Ref Expression
Assertion ccref class CovHasRef 𝐴