case h.mk
α : Type ?u.31962
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
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) (Quot.mk Setoid.r a✝) =
    (map g h1 ∘ map f h2) (Quot.mk Setoid.r a✝)
α : Type ?u.31962
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
h1 : LEComap g B C
h2 : LEComap f A B
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) = map g h1 ∘ map f h2
ext ⟨⟩
no goals
case h.mk
α : Type ?u.31962
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
h1 : LEComap g B C
h2 : LEComap f A B
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.comp g f) (_ : LEComap (ContinuousMap.comp g f) A C) (Quot.mk Setoid.r a✝) =
    (map g h1 ∘ map f h2) (Quot.mk Setoid.r a✝)
rfl