Zulip Chat Archive

Stream: new members

Topic: trivial topology


view this post on Zulip 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 }

view this post on Zulip 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)

view this post on Zulip 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 },

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 21 2020 at 13:51):

No

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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