# Zulip Chat Archive

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

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

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,
by_contradiction contra,
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_separated`

means

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