α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformContinuous f
a : α
⊢ (Quotient.mk' ∘ f) a = Quotient.mk (separationSetoid β) (f a)
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformContinuous f
a : α
⊢ map f (Quotient.mk (separationSetoid α) a) = Quotient.mk (separationSetoid β) (f a)
rw [map, lift_mk (uniformContinuous_quotient_mk'.comp h)]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformContinuous f
a : α
⊢ (Quotient.mk' ∘ f) a = Quotient.mk (separationSetoid β) (f a)
rfl