α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x => 1 / f x
⊢ UniformContinuous fun x => (f x)⁻¹
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x => (f x)⁻¹
have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
no goals
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x => 1 / f x
⊢ UniformContinuous fun x => (f x)⁻¹
simp_all