## Stream: general

### Topic: T2 space

#### Kenny Lau (Oct 24 2018 at 16:29):

Why isn't T2 space a Prop?

it should be

#### 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)


#### Chris Hughes (Oct 29 2018 at 10:51):

Aren't they the same?

#### Patrick Massot (Oct 29 2018 at 10:55):

Blind guess: they are not constructively the same

#### Patrick Massot (Oct 29 2018 at 10:56):

Now I'll read the two definitions

#### Patrick Massot (Oct 29 2018 at 10:58):

My vote: keep the current definition

#### 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.

#### 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?

#### 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

#### 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