α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) =
    comap ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 γ)
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) = 𝓤 α
rw [← hf.1, ← hg.1, comap_comap]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) =
    comap ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 γ)
rfl