Zulip Chat Archive

Stream: new members

Topic: Discrete topology?


view this post on Zulip Pedro Minicz (Aug 15 2020 at 22:46):

Where is the definition of the discrete topology on a type α? There is a definition of discrete topology predicate here. It defines it as being equal to the bottom element of some order. I am struggling to make sense of this definition and don't seem to find the definition of the bottom element itself (it is implicitly declared somewhere I believe).

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:48):

You could look for #check (by apply_instance : has_bot (topological_space A))

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:50):

It looks like it's coming from src#topological_space.complete_lattice, in a bit of abstract nonsense

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:52):

In short, it reduces to univ

view this post on Zulip Pedro Minicz (Aug 15 2020 at 22:56):

Mario Carneiro said:

In short, it reduces to univ

What exactly do you mean it reduces to univ? I know that is_open = univ is this topology, but I don't see how that term can reduce to univ.

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:57):

it's pretty involved. Where are you stuck?

view this post on Zulip Pedro Minicz (Aug 15 2020 at 22:57):

I managed to complete the goal I was working on with a single simp and honestly I am not quite sure how it worked.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 22:58):

import topology.order
import tactic

variables {α : Type*}

namespace cofinite

@[simp] def is_open : set α  Prop :=
λ s, set.finite (set.univ \ s)  s = 

lemma is_open_univ : is_open (set.univ : set α) :=
begin
  unfold is_open,
  left,
  rw set.diff_self,
  exact set.finite_empty
end

lemma is_open_inter (s₁ s₂ : set α) :
  is_open s₁  is_open s₂  is_open (s₁  s₂) :=
begin
  rintros (hs₁ | hs₁) (hs₂ | hs₂),
  { unfold is_open,
    left,
    rw set.diff_inter,
    exact set.finite.union hs₁ hs₂ },
  all_goals { right, simp [hs₁, hs₂] }
end

lemma is_open_sUnion (s : set (set α)) (hs :  t, t  s  is_open t) :
  is_open (⋃₀ s) :=
begin
  by_cases h :  t, t  s  t  ,
  { unfold is_open,
    left,
    rcases h with t, ht₁, ht₂,
    have ht₂ : set.finite (set.univ \ t),
    { cases hs t ht₁ with ht₃ ht₃,
      { exact ht₃ },
      { exfalso, exact ht₂ ht₃ } },
    apply set.finite.subset ht₂,
    intros x hx,
    suffices : x  t, { simpa },
    simp at hx,
    exact hx t ht₁ },
  { push_neg at h,
    unfold is_open,
    right,
    ext x,
    suffices :  t, t  s  x  t, { simpa },
    intros t ht,
    specialize h t ht,
    rw set.eq_empty_iff_forall_not_mem at h,
    exact h x }
end

@[simp] instance topological_space (α : Type*) : topological_space α :=
{ is_open := is_open,
  is_open_univ := is_open_univ,
  is_open_inter := is_open_inter,
  is_open_sUnion := is_open_sUnion }

example [fintype α] : discrete_topology α :=
begin
  constructor,
  ext s,
  split; intro hs,
  -- I have no idea what the following `simp` is doing.
  { simp only [topological_space.is_open] at hs },
  { left, apply set.finite.of_fintype }
end

end cofinite

view this post on Zulip Pedro Minicz (Aug 15 2020 at 22:58):

A bit long, the goal is the last example.

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:59):

The simp only is smoke and mirrors, the proof is trivial

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:00):

It would be good to have a simp lemma that says \bot.is_open s though

view this post on Zulip Pedro Minicz (Aug 15 2020 at 23:01):

Ah, of course!

view this post on Zulip Pedro Minicz (Aug 15 2020 at 23:01):

Mario Carneiro said:

It would be good to have a simp lemma that says \bot.is_open s though

Yes, that would be quite convenient.

view this post on Zulip Pedro Minicz (Aug 15 2020 at 23:02):

Isn't it curious that simp doesn't close the trivial goal?

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 23:04):

It's not an equality

view this post on Zulip Floris van Doorn (Aug 15 2020 at 23:55):

simp doesn't unfold definitions, unless it is told to (by attributes or when you invoke it). So simp doesn't know the goal is trivial.

view this post on Zulip Floris van Doorn (Aug 15 2020 at 23:56):

There are plenty of times when simp doesn't close a goal, but refl or exact trivial does (sometimes that means more things should be simp-lemmas)

view this post on Zulip Patrick Massot (Aug 16 2020 at 00:00):

docs#is_open_discrete

view this post on Zulip Mario Carneiro (Aug 16 2020 at 00:35):

The irony is that even though simp proves things by reducing them to true, simp will fail on the goal true


Last updated: May 08 2021 at 10:12 UTC