surprisingly fiddly

Stream: Lean for the curious mathematician 2020

[Alistair Tucker]

Hi! Exercise 3 on topological spaces says:

Define the indiscrete topology on any type using this.
(To do it without this it is surprisingly fiddly to prove that the set {∅, univ} actually forms a topology)

Is that to say it is surprisingly fiddly to do without using an inductive type?

[Alex J. Best]

Yes, to prove that {∅, univ} is a topology in the same way that I prove the discrete topology is a topology in that file (not cheating and saying the smallest thing generated by it) I found far longer than I expected.

[Alistair Tucker]

Does that mean we are now missing the fact that it is the coarsest topology?

[Alex J. Best]

Yes we haven't proved that {∅, univ} itself is actually a topology, just constructed some topology whose open sets we don't have that explicit description for.

[Mario Carneiro]

We know that there is a coarsest topology, and that it is generate_from empty

[Kevin Buzzard]

@Floris van Doorn worked through a proof of this during this afternoon's session

[Alistair Tucker]

Thanks.

[David Wärn]

{∅, univ} might be the first definition of the indiscrete topology you'll think of, but another definition like is_open A ↔ ∀ x y, x ∈ A → y ∈ A might be easier to work with

[Alex J. Best]

Yes my definition could be an artifact of the fact I originally set up the demo file using set (set X) rather than set X \to Prop before noticing the latter worked better.