Metamath Proof Explorer


Syntax definition cphtpy

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

Ref Expression
Assertion cphtpy class PHtpy