# Zulip Chat Archive

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

#### Pedro Minicz (Aug 15 2020 at 23:01):

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

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