no goals
F : Type ?u.344889
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
S : Set X
⊢ ∀ {x y : C(X, Y)}, HomotopicRel x y S → HomotopicRel y x S
apply symm
no goals
F : Type ?u.344889
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
S : Set X
⊢ ∀ {x y z : C(X, Y)}, HomotopicRel x y S → HomotopicRel y z S → HomotopicRel x z S
apply trans