α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1) (Quotient.mk (separationSetoid α) a) = f a
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ lift f (Quotient.mk (separationSetoid α) a) = f a
rw [lift, dif_pos h]
no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1) (Quotient.mk (separationSetoid α) a) = f a
rfl