## Stream: Is there code for X?

### Topic: totally disconnected of discrete

#### Adam Topaz (Nov 08 2020 at 19:09):

apply_instance fails for the following. Is this instance missing?

import topology.subset_properties

variables (α : Type*) [topological_space α] [discrete_topology α]

example : totally_disconnected_space α := sorry


probably

#### Adam Topaz (Nov 08 2020 at 19:24):

Okay, I have an ugly proof. I'm sure someone who is more familiar with the discrete_topology and/or totally_disconnected_space api can come up with a 1-liner:

import topology.subset_properties

variables (α : Type*) [topological_space α] [discrete_topology α]

open_locale classical

example : totally_disconnected_space α :=
begin
constructor,
intros T hT h1,
constructor,
intros x y,
specialize h1 {x} (set.univ \ {x}) (is_open_discrete _) (is_open_discrete _) _ _ _,
rcases h1 with ⟨t,ht⟩,
finish,
finish,
use x,
finish,
use y,
simp,
intro c,
apply contra,
ext,
symmetry,
assumption,
end


#### Mario Carneiro (Nov 08 2020 at 19:27):

I see that in the same file there is also totally_separated, which also seems like it would be true for a discrete space and implies totally_disconnected

#### Adam Topaz (Nov 08 2020 at 19:28):

I have no idea what totally_separatedmeans

#### Mario Carneiro (Nov 08 2020 at 19:28):

the FOL description is there in the definition

#### Mario Carneiro (Nov 08 2020 at 19:29):

I don't have any deep understanding of the term but those symbols look true

#### Mario Carneiro (Nov 08 2020 at 19:30):

and more to the point it looks a bit easier to prove those symbols than the ones in totally_disconnected

#### Mario Carneiro (Nov 08 2020 at 19:33):

example : totally_separated_space α :=
⟨λ a _ b _ h, ⟨{b}ᶜ, {b}, is_open_discrete _, is_open_discrete _, by simpa⟩⟩


#### Adam Topaz (Nov 08 2020 at 19:36):

Funny, I used {a} and {a}\^c, instead of {b}^\c and {b}, and ended up with a messy proof again!

#### Mario Carneiro (Nov 08 2020 at 19:37):

yep I started with that but then you have to throw in commutativity because a \in {b}^c unfolds to b != a

#### Adam Topaz (Nov 08 2020 at 19:37):

Anyway, can you PR this?

#### Adam Topaz (Nov 08 2020 at 19:41):

Oooh, that doesn't even require classical!

#### Mario Carneiro (Nov 08 2020 at 19:42):

it does, you have to prove {b}^c \cup {b} = univ

#### Adam Topaz (Nov 08 2020 at 19:43):

Oh right

Last updated: May 16 2021 at 05:21 UTC