## Stream: maths

### Topic: totally_disconnected uses subsingleton, not set.subsingleton

#### Bryan Gin-ge Chen (Feb 14 2021 at 01:59):

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 (Feb 14 2021 at 02:05):

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

#### Yury G. Kudryashov (Feb 14 2021 at 07:34):

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.

Last updated: May 18 2021 at 07:19 UTC