Pushforward(?) topology

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have the following construction? (It's a mild generalization of the quotient topology.)

import data.set.basic
import topology.basic

variables {α β : Type*} [topological_space α] (f : α → β)

example : topological_space β :=
{ is_open := λ X, is_open $ f ⁻¹' X,
  is_open_univ := by simp,
  is_open_inter := λ _ _ h1 h2, is_open_inter h1 h2,
  is_open_sUnion := sorry }

[Patrick Massot]

docs#topological_space.coinduced

[Adam Topaz]

Perfect! Thanks :)