trivial topology

Stream: new members

[Jia Ming]

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]

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]

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

[Jia Ming]

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

[Reid Barton]

No

[Jia Ming]

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]

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

[Andreas Steiger]

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]

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]

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]

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.