Disjoint union of totally disconnected spaces

Stream: Is there code for X?

[Bhavik Mehta]

instance {α β : Type*} [topological_space α] [topological_space β]
  [totally_disconnected_space α] [totally_disconnected_space β] :
  totally_disconnected_space (α ⊕ β) :=

Do we have something resembling this in mathlib?

[Johan Commelin]

I'm not aware of it

[Kevin Buzzard]

Should one prove it for any top space which satisfies the universal property of the disjoint union?

[Kevin Buzzard]

oh, perhaps one could prove this instance first and then deduce the general one from it.

[Floris van Doorn]

It's definitely not an instance: docs#totally_disconnected_space.

[Adam Topaz]

I guess it should be done for docs#totally_separated_space as well...

[Adam Topaz]

(deleted)