Stream: new members

Topic: Discrete topology?

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).

Mario Carneiro (Aug 15 2020 at 22:48):

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

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

Mario Carneiro (Aug 15 2020 at 22:52):

In short, it reduces to univ

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.

Mario Carneiro (Aug 15 2020 at 22:57):

it's pretty involved. Where are you stuck?

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.

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

Pedro Minicz (Aug 15 2020 at 22:58):

A bit long, the goal is the last example.

Mario Carneiro (Aug 15 2020 at 22:59):

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

Mario Carneiro (Aug 15 2020 at 23:00):

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

Ah, of course!

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.

Pedro Minicz (Aug 15 2020 at 23:02):

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

Kevin Buzzard (Aug 15 2020 at 23:04):

It's not an equality

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.

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)

Patrick Massot (Aug 16 2020 at 00:00):

docs#is_open_discrete

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