case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift f)

case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift f)
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
⊢ UniformContinuous (lift f)
by_cases hf : UniformContinuous f
case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1))
case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (lift f)
rw [lift, dif_pos hf]
no goals
case pos
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → f x = f x_1))
exact uniformContinuous_quotient_lift hf
case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (Nonempty.some (_ : Nonempty α))
case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift f)
rw [lift, dif_neg hf]
no goals
case neg
α : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (Nonempty.some (_ : Nonempty α))
exact uniformContinuous_of_const fun a _ => rfl