α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map (fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ UniformContinuous f ↔ UniformContinuous (g ∘ f)
dsimp only [UniformContinuous, Tendsto]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 γ ↔
    map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map (fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 γ ↔
    map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
rfl