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.

[Bjørn Kjos-Hanssen]

Just came across this old thread, and relatedly:

I know the trivial topology on Fin 2 exists by the name of ⊤, but I wasn't able to use it to prove

 ¬ (⊤ : TopologicalSpace (Fin 2)).IsOpen {0}

So I rolled my own, dropping it here in case it's useful (or someone knows how to avoid it):

import Mathlib.Topology.Defs.Basic
import Mathlib.MeasureTheory.Measure.Hausdorff
import Mathlib.Topology.Defs.Basic
def mytop : TopologicalSpace (Fin 2) :=
{
  IsOpen := λ S ↦ S = ∅ ∨ S = Set.univ
  isOpen_univ := Or.inr rfl
  isOpen_inter := by
    intro S T hS hT
    cases hS with
    |inl h => subst h;left;simp
    |inr h =>
      subst h
      cases hT with
      |inl h => subst h;left;simp
      |inr h => subst h;right;simp
  isOpen_sUnion := by
    intro S hS
    simp at hS
    by_cases H : Set.univ ∈ S
    . right;refine Set.sUnion_eq_univ_iff.mpr ?_;
      intro a;exists Set.univ
    . left
      have : ∀ t ∈ S, t = ∅ := by
        intro t ht
        let Q := hS t ht
        cases Q with
        |inl h => tauto
        |inr h => subst h;tauto
      exact Set.sUnion_eq_empty.mpr this
}

[Eric Wieser]

Here's a proof of the original statement:

example : ¬ (⊤ : TopologicalSpace (Fin 2)).IsOpen {0} := by
  change ¬@IsOpen (Fin 2) ⊤ {0}  -- fix the weird spelling so that we can use lemmas
  rw [TopologicalSpace.isOpen_top_iff]
  simp only [Set.singleton_ne_empty, false_or]
  intro h
  cases h.ge (Set.mem_univ 1)

[Eric Wieser]

Your mistake was writing (⊤ : TopologicalSpace (Fin 2)).IsOpen instead of ¬IsOpen (Fin 2) ⊤

[Eric Wieser]

It's the same mistake as writing Nat.add n 1 instead of n + 1, since all the lemmas are only about the latter

[Eric Wieser]

docs#TopologicalSpace.isOpen_top_iff is obviously the key here, but it's hard to tell what its statement really is without looking at the source

[Bjørn Kjos-Hanssen]

OK great... sorry for the "weird spelling" :)

[Eric Wieser]

No worries, clearly we have a documentation failure here

[Eric Wieser]

Maybe your spelling should be the preferred one after all? We could add export TopologicalSpace (IsOpen), and then the two spellings would mean the same thing

[Eric Wieser]

Perhaps @Yury G. Kudryashov or @Sébastien Gouëzel or @Patrick Massot have opinions here?

[Bjørn Kjos-Hanssen]

Thanks @Eric Wieser For what it's worth, I probably wrote it that way because I was trying (and now succeeded) to prove

∃ ( σ τ : TopologicalSpace (Fin 2)), σ.IsOpen ≠ τ.IsOpen

[Eric Wieser]

Yes, you shouldn't write that either!

[Eric Wieser]

∃ ( σ τ : TopologicalSpace (Fin 2)), @IsOpen _ σ ≠ @IsOpen _ τ

[Yury G. Kudryashov]

If we export, then we need to use the prefix TopologicalSpace.IsOpen for dot notation theorems.

[Yury G. Kudryashov]

We have notation IsOpen[t]

[Patrick Massot]

Yes, the solution is to use the notation.