Metamath Proof Explorer


Syntax definition chtpy

Description: Extend class notation with the class of homotopies between two continuous functions.

Ref Expression
Assertion chtpy class Htpy