Zulip Chat Archive

Stream: general

Topic: T2 space


view this post on Zulip Kenny Lau (Oct 24 2018 at 16:29):

Why isn't T2 space a Prop?

view this post on Zulip Reid Barton (Oct 24 2018 at 16:41):

it should be

view this post on Zulip Kenny Lau (Oct 29 2018 at 10:47):

I think the current definition is wrong:

class t2_space (α : Type u) [topological_space α] : Prop :=
(t2 : x y, x  y  u v : set α, is_open u  is_open v  x  u  y  v  u  v = )

I think the right one should be:

class t2_space (α : Type u) [topological_space α] : Prop :=
(t2 : x y, (u v : set α, is_open u  is_open v  x  u  y  v   r, r  u  v)  x = y)

view this post on Zulip Chris Hughes (Oct 29 2018 at 10:51):

Aren't they the same?

view this post on Zulip Patrick Massot (Oct 29 2018 at 10:55):

Blind guess: they are not constructively the same

view this post on Zulip Patrick Massot (Oct 29 2018 at 10:56):

Now I'll read the two definitions

view this post on Zulip Patrick Massot (Oct 29 2018 at 10:58):

My vote: keep the current definition

view this post on Zulip Kevin Buzzard (Oct 29 2018 at 13:11):

Presumably one of them implies the other constructively? Maybe the weaker one should be T1.9999999..., which presumably is not constructively equal to 2.

view this post on Zulip Kevin Buzzard (Oct 29 2018 at 13:14):

More seriously, even though this definition is in a file with local attribute [instance] prop_decidable right at the top, maybe there is a case for calling one of them t2_space' or something?

view this post on Zulip Reid Barton (Oct 29 2018 at 13:47):

I think it's usually better to have a theorem t2_iff_kenny, rather than two equivalent definitions

view this post on Zulip Reid Barton (Oct 29 2018 at 14:04):

that is, assuming the purpose is that the kenny characterization is easier to work with for some purposes


Last updated: May 15 2021 at 23:13 UTC