## Stream: new members

### Topic: trivial topology

#### Jia Ming (Oct 21 2020 at 13:29):

Hello, this is another easy exercise that I got stuck on. Any hints on solving the sorry? It boils down to doing cases on S ⊆ {∅, univ} I think, but I don't know how to go about it in Lean.

import tactic
open set

structure topology :=
(X : Type)
(τ : set (set X))
(has_univ : univ ∈ τ)
(has_sUnion : ∀ S ⊆ τ, ⋃₀ S ∈ τ)
(has_inter : ∀ U₁ U₂ ∈ τ, U₁ ∩ U₂ ∈ τ)

def trivial_topology : topology :=
{ X := ℚ,
τ := {∅, univ},
has_univ := by simp,
has_sUnion := sorry,
has_inter := by finish }


#### Reid Barton (Oct 21 2020 at 13:36):

This might be considered overkill but I think I would first prove a lemma like s ∈ {∅, univ} <-> \ex p, (\all x, (x ∈ s) <-> p)

#### Andreas Steiger (Oct 21 2020 at 13:43):

I'd probably use a structure like  has_sUnion := by { rintros S hs, by_cases univ ∈ S, sorry },

#### Jia Ming (Oct 21 2020 at 13:50):

Reid Barton said:

This might be considered overkill but I think I would first prove a lemma like s ∈ {∅, univ} <-> \ex p, (\all x, (x ∈ s) <-> p)

Did you mean s ⊆ {∅, univ} <-> \ex p, (\all x, (x ∈ s) <-> p)? Cuz it doesn't check out haha

No

#### Jia Ming (Oct 21 2020 at 13:53):

Andreas Steiger said:

I'd probably use a structure like  has_sUnion := by { rintros S hs, by_cases univ ∈ S, sorry },

I got as far as

  has_sUnion := begin
intros S hS,
by_cases h₁ : S = ∅, simp * at *,
by_cases h₂ : S = {∅}, simp * at *,
by_cases h₃ : S = {univ}, simp * at *,
by_cases h₄ : S = {∅, univ}, simp * at *,
exfalso,
sorry,
end,


left with the goal, which seems sooo close. but im completely lost

S : set (set ℚ),
hS : S ⊆ {∅, univ},
h₁ : ¬S = ∅,
h₂ : ¬S = {∅},
h₃ : ¬S = {univ},
h₄ : ¬S = {∅, univ}
⊢ false


#### Kevin Buzzard (Oct 21 2020 at 13:57):

Reid is suggesting that an arbitrary union of subsets corresponding to constant predicates is also a subset corresponding to a constant predicate.

#### Andreas Steiger (Oct 21 2020 at 13:57):

Using by_cases you shouldn't need to do all 4, because every by_cases splits up in 2 anyway. If you do by_cases univ ∈ S, you get two goals: Prove the statement if univ \in S, and prove the statement if univ \notin S. These should suffice, no need to split up further.

#### Kevin Buzzard (Oct 21 2020 at 14:16):

import tactic

example (X : Type) (a b : X) (S : set X) (hS : S ⊆ {a, b}) :
S = ∅ ∨ S = {a} ∨ S = {b} ∨ S = {a,b} :=
begin
by_cases ha : a ∈ S;
by_cases hb : b ∈ S,
{ right, right, right,
ext x,
split, apply hS,
finish },
{ right, left,
ext x,
split,
{ intro hx,
specialize hS hx,
finish },
{ finish }
},
{ right, right, left,
ext x,
split,
{ intro hx,
specialize hS hx,
finish },
{ finish } },
{ left,
ext x,
split,
{ intro hx,
specialize hS hx,
finish },
{ finish } }
end


#### Kevin Buzzard (Oct 21 2020 at 14:18):

Of course it would be rather less fun doing this for a set of size 4. For some stuff like this there are tactics, e.g. tactic#fin_cases, but I'm not sure about this one.

#### Jia Ming (Oct 21 2020 at 14:23):

Omg this is awesome! Thank you all so much, now I got two ways to prove it!

Also, what I meant by 'couldn't check out' was I didn't know how to fix the error that lean kept giving. Turns out that it just couldn't guess the type of {∅, univ}, not that I doubted your lemma hahah no idea how you came up with it but it's amazing.

Last updated: May 06 2021 at 21:09 UTC