totally_disconnected uses subsingleton, not set.subsingleton

Stream: maths

[Bryan Gin-ge Chen]

I'm hacking on #6188 and I noticed that src#is_totally_disconnected uses docs#subsingleton (on types) rather than docs#set.subsingleton:

def is_totally_disconnected (s : set α) : Prop :=
∀ t, t ⊆ s → is_preconnected t → subsingleton t -- why not `t.subsingleton` here?

This seems to lead to a bunch of uses of docs#set.subsingleton_coe throughout. Would replacing subsingleton with set.subsingleton be an improvement?

[Bryan Gin-ge Chen]

Oh, it's not so clear... docs#set.subsingleton_of_image uses subsingleton on types too.

[Yury G. Kudryashov]

set.subsingleton is a relatively new addition to mathlib, so I'm not surprised that some coded uses _root_.subsingleton instead. I think that rewriting this code in terms of set.subsingleton is a good idea.