Discrete topology?

Stream: new members

[Pedro Minicz]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

In short, it reduces to univ

[Pedro Minicz]

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]

it's pretty involved. Where are you stuck?

[Pedro Minicz]

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]

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]

A bit long, the goal is the last example.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Pedro Minicz]

Ah, of course!

[Pedro Minicz]

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]

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

[Kevin Buzzard]

It's not an equality

[Floris van Doorn]

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]

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]

docs#is_open_discrete

[Mario Carneiro]

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