initial topology

Stream: general

[Anas Himmi]

is this a good way to define the initial topology?

import topology.order

open topological_space

variables {α : Type*} {β : Type*}

def initial_topology  (Y:β → Type*) (T:Π b:β,topological_space (Y b)) (f:Π b:β, (α → (Y b))) : topological_space α :=
generate_from {V | ∃ (b:β) (U) (hU:is_open (T b) U),V=(f b)⁻¹'U}

[Mario Carneiro]

I think you can use the lattice operations to define this

[Mario Carneiro]

def initial_topology (Y : β → Type*) (T : Π b, topological_space (Y b)) (f : Π b, α → Y b) :
  topological_space α := ⨆ b, induced (f b) (T b)

[Anas Himmi]

Thank you!

[Nicolò Cavalleri]

Was this PRed under some namespace if it was PRed? I cannot find it