α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ UniformInducing f
refine' ⟨le_antisymm _ hf.le_comap⟩
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
exact comap_mono hg.le_comap