Bryan Gin-ge Chen (Feb 14 2021 at 01:59):
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
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