Zulip Chat Archive

Stream: maths

Topic: totally_disconnected uses subsingleton, not set.subsingleton


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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