no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.717
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ inst✝³ ≤ induced f inst✝²
rwa [← continuous_iff_le_induced]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.717
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝¹)
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.717
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝³
rw [hgf.induced, ← induced_compose]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.717
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
g : β → γ
hf : Continuous f
hg : Continuous g
hgf : Inducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝¹)
exact induced_mono hg.le_induced