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