Zulip Chat Archive

Stream: Is there code for X?

Topic: totally disconnected of discrete


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 08 2020 at 19:10):

probably

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 08 2020 at 19:28):

I have no idea what totally_separatedmeans

view this post on Zulip Mario Carneiro (Nov 08 2020 at 19:28):

the FOL description is there in the definition

view this post on Zulip Mario Carneiro (Nov 08 2020 at 19:29):

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

view this post on Zulip 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

view this post on Zulip 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⟩⟩

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 08 2020 at 19:37):

Anyway, can you PR this?

view this post on Zulip Adam Topaz (Nov 08 2020 at 19:41):

Oooh, that doesn't even require classical!

view this post on Zulip Mario Carneiro (Nov 08 2020 at 19:42):

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

view this post on Zulip Adam Topaz (Nov 08 2020 at 19:43):

Oh right


Last updated: May 16 2021 at 05:21 UTC