α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous fun p => p.fst / p.snd
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
⊢ UniformContinuous fun p => p.fst / p.snd
letI : UniformSpace β := u.comap f
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous (↑f ∘ fun p => p.fst / p.snd)
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous fun p => p.fst / p.snd
refine' uniformContinuous_comap' _
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous fun x => ↑f x.fst / ↑f x.snd
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous (↑f ∘ fun p => p.fst / p.snd)
simp_rw [Function.comp, map_div]
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous ((fun p => p.fst / p.snd) ∘ Prod.map ↑f ↑f)
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous fun x => ↑f x.fst / ↑f x.snd
change UniformContinuous ((fun p : γ × γ => p.1 / p.2) ∘ Prod.map f f)
no goals
α : Type ?u.119518
β : Type u_3
inst✝⁶ : UniformSpace α
inst✝⁵ : Group α
inst✝⁴ : UniformGroup α
inst✝³ : Group β
γ : Type u_1
inst✝² : Group γ
u : UniformSpace γ
inst✝¹ : UniformGroup γ
F : Type u_2
inst✝ : MonoidHomClass F β γ
f : F
this : UniformSpace β := UniformSpace.comap (↑f) u
⊢ UniformContinuous ((fun p => p.fst / p.snd) ∘ Prod.map ↑f ↑f)
exact uniformContinuous_div.comp (uniformContinuous_comap.prod_map uniformContinuous_comap)