T2 space

Stream: general

[Kenny Lau]

Why isn't T2 space a Prop?

[Reid Barton]

it should be

[Kenny Lau]

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]

Aren't they the same?

[Patrick Massot]

Blind guess: they are not constructively the same

[Patrick Massot]

Now I'll read the two definitions

[Patrick Massot]

My vote: keep the current definition

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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