totally disconnected of discrete

Stream: Is there code for X?

[Adam Topaz]

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]

probably

[Adam Topaz]

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]

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]

I have no idea what totally_separatedmeans

[Mario Carneiro]

the FOL description is there in the definition

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Adam Topaz]

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

[Mario Carneiro]

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

[Adam Topaz]

Anyway, can you PR this?

[Adam Topaz]

Oooh, that doesn't even require classical!

[Mario Carneiro]

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

[Adam Topaz]

Oh right