Zulip Chat Archive

Stream: Is there code for X?

Topic: Pushforward(?) topology


view this post on Zulip Adam Topaz (Sep 24 2020 at 13:46):

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 }

view this post on Zulip Patrick Massot (Sep 24 2020 at 13:47):

docs#topological_space.coinduced

view this post on Zulip Adam Topaz (Sep 24 2020 at 13:48):

Perfect! Thanks :)


Last updated: May 16 2021 at 05:21 UTC