α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.137691
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝³) ≤ coinduced g inst✝²
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.137691
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ inst✝¹ ≤ coinduced g inst✝²
rw [hgf.right, ← coinduced_compose]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.137691
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : β → γ
f : α → β
hf : Continuous f
hg : Continuous g
hgf : QuotientMap (g ∘ f)
⊢ coinduced g (coinduced f inst✝³) ≤ coinduced g inst✝²
exact coinduced_mono hf.coinduced_le