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