Continuity and inducing

Stream: Is there code for X?

[Thomas Browning]

Is this lemma in mathlib, or is there an easier proof using mathlib?

import topology.order

example (W X Y Z : Type*) [topological_space W] [topological_space X] [topological_space Y]
  [topological_space Z] (f : X → Y) (g : W → Z) (i : W → X) (j : Z → Y)
  (hi : inducing i) (hj : inducing j) (h : f ∘ i = j ∘ g) (hg : continuous f) :
  continuous g :=
begin
  rw [continuous_iff_le_induced, hj.induced, induced_compose, ←h, ←induced_compose],
  rw continuous_iff_le_induced at hg,
  rw hi.induced,
  exact induced_mono hg,
end

[Patrick Massot]

example (W X Y Z : Type*) [topological_space W] [topological_space X] [topological_space Y]
  [topological_space Z] (f : X → Y) (g : W → Z) (i : W → X) (j : Z → Y)
  (hi : inducing i) (hj : inducing j) (h : f ∘ i = j ∘ g) (hg : continuous f) :
  continuous g :=
begin
  rw [hj.continuous_iff, ← h],
  exact hg.comp hi.continuous,
end

[Patrick Massot]

It would have been faster if hg had been named hf

[Patrick Massot]

Also note the assumption on i is way too strong, continuity is enough.