no goals
α : Type ?u.26859
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
f : C(X, Y)
A A' : DiscreteQuotient X
B B' : DiscreteQuotient Y
g : C(Y, Z)
C : DiscreteQuotient Z
⊢ LEComap g B C → LEComap f A B → LEComap (ContinuousMap.comp g f) A C
tauto