case h.mk
α : Type ?u.31713
X : Type u_1
Y : Type ?u.31719
Z : Type ?u.31722
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
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
α : Type ?u.31713
X : Type u_1
Y : Type ?u.31719
Z : Type ?u.31722
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
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) = id
ext ⟨⟩
no goals
case h.mk
α : Type ?u.31713
X : Type u_1
Y : Type ?u.31719
Z : Type ?u.31722
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
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) (_ : LEComap (ContinuousMap.id X) A A) (Quot.mk Setoid.r a✝) = id (Quot.mk Setoid.r a✝)
rfl