α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.5084
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous f
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.5084
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
⊢ Inducing f ↔ Inducing (g ∘ f)
refine' ⟨fun h => hg.comp h, fun hgf => inducing_of_inducing_compose _ hg.continuous hgf⟩
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.5084
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous (g ∘ f)
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.5084
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous f
rw [hg.continuous_iff]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.5084
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hg : Inducing g
hgf : Inducing (g ∘ f)
⊢ Continuous (g ∘ f)
exact hgf.continuous