Working with choose!

Stream: new members

[Callum Cassidy-Nolan]

Hi there, I'm struggling to get my proof to work, I'm working on this topology question:

image.png

The outline of the proof is that you can write A as a union of x in A, U_x (where U_x) is open wrt X, then we know that as a union of open sets A itself must be open as well.

I'm still having some difficulties in the first half, which would just be showing that A is the union. To start my proof I'm trying to use choose or choose! but either one seems to lead to an error later on in the proof, here's what I have as of yet:

import topology.basic

variables {X : Type} [topological_space X] {A: set X}

theorem munkres_13_1
  (h₀ : ∀ x ∈ A, ∃ U : set X, is_open U ∧ x ∈ U ∧ U ⊆ A)
  :
  is_open A
  :=
begin
  choose f h_f using h₀,
  have a_equals : A = set.Union f :=
  begin
    ext x,
    split,
    {
      intro h_A,
      rw set.mem_Union,
      use x,
      exact (h_f x h_A).2.1,
    },
    {
      intro h_u,
      rw set.mem_Union at h_u,
      cases h_u with a h_a,
      have h_f_a_sbs := (h_f a),
      exact set.mem_of_subset_of_mem h_f_a_sbs h_a,
    }
  end
end

In this state, we have the problem that set.Union f won't work because f has the type f: Π (x : X), x ∈ A → set X instead of f: A -> X.

Thanks for taking a look.

[Matt Diamond]

I think what you need here is Union₂... instead of A = set.Union f, try A = ⋃ x h, f x h

[Matt Diamond]

and you can use set.mem_Union₂ instead of set.mem_Union

[Matt Diamond]

though there doesn't seem to be an is_open_Union₂ lemma, so the end of the proof might be a little inelegant... perhaps there's a better solution

[Mario Carneiro]

you should just be able to use union lemmas twice

[Mario Carneiro]

but also, in case you weren't aware @Callum Cassidy-Nolan you can prove this one without choice by just taking the union of all open subsets of A

[Mario Carneiro]

alternatively, since you have topology.basic imported you can just use this theorem itself, which is of course proved (as docs#is_open_iff_forall_mem_open)

[Callum Cassidy-Nolan]

Ah, I see what you are saying! Thanks for the tips. I managed to get this part of the proof:

theorem munkres_13_1
  (h₀ : ∀ x ∈ A, ∃ U : set X, is_open U ∧ x ∈ U ∧ U ⊆ A)
  :
  is_open A
  :=
begin
  choose f h_f using h₀,
  have a_equals : A = ⋃ x h, f x h :=
  begin
    ext x,
    split,
    {
      intro h_A,
      rw set.mem_Union₂,
      use x,
      use h_A,
      exact (h_f x h_A).2.1,
    },
    {
      intro h_u,
      rw set.mem_Union₂ at h_u,
      cases h_u with a h_a,
      cases h_a with h_a h_x_mem,
      have h_f_a_sbs := (h_f a h_a).2.2,
      exact set.mem_of_subset_of_mem h_f_a_sbs h_x_mem,
    },
  end
end

[Matt Diamond]

a couple syntax tips, in case you don't know:

1) instead of two use statements, you can write use [x, h_A] on one line
2) instead of two cases statements, you can write rcases h_u with ⟨a, h_a, h_x_mem⟩ to deconstruct everything at once

[Callum Cassidy-Nolan]

Matt Diamond said:

a couple syntax tips, in case you don't know:

1) instead of two use statements, you can write use [x, h_A] on one line
2) instead of two cases statements, you can write rcases h_u with ⟨a, h_a, h_x_mem⟩ to deconstruct everything at once

Thanks, that helps me ! I also just think I realized that proving what I just did doesn't quite match the topology definition for union since it requires a set of subsets of the topological space: image.png

[Matt Diamond]

hmm

[Matt Diamond]

I mean I think you defined it correctly according to the problem text you posted originally

[Matt Diamond]

the set of subsets is the range of your choice function f, and you took the union of that

[Callum Cassidy-Nolan]

So in order to satisfy the definition of topology in mathlib I need to create something like this right: let s : set (set X) = {f x (h : x ∈ A) | x ∈ A},?

[Matt Diamond]

I'm probably not the best person to answer this (I'm better with basic questions :sweat_smile:) but I'm curious what you mean by "satisfy the definition of topology in mathlib"... your proof correctly proved that A is an open set in the topology on X

[Callum Cassidy-Nolan]

So far in my proof I've shown that A = ⋃ x h, f x h, but in order to show that A is open, I need to use the fact that arbitrary unions of open sets are open, which comes from this part of the definition of topology: image.png

[Callum Cassidy-Nolan]

So to use that fact I would have to write something like exact is_open_sUnion s ... which would finish the proof of showing A is open.

[Matt Diamond]

oh yeah, you can still do that with the way you've written it out, there's no need to go back and fix things

[Matt Diamond]

one way to go about it, once you rewrite the goal using your equality, is to do apply is_open_Union and intro a couple of times

[Callum Cassidy-Nolan]

Since is_open_Union requires a function like this: image.png

But the function I have is f: Π (x : X), x ∈ A → set X I would have to define a new function which matches this type right?

How do you go about defining a function mid way through a proof like this?

[Matt Diamond]

it's not too difficult to define a function, but I don't think you necessarily need to do that... take a look at this:

import topology.basic

variables {X : Type} [topological_space X] {A: set X}

theorem munkres_13_1
  (h₀ : ∀ x ∈ A, ∃ U : set X, is_open U ∧ x ∈ U ∧ U ⊆ A)
  :
  is_open A
  :=
begin
  choose f h_f using h₀,
  have a_equals : A = ⋃ x h, f x h :=
  begin
    ext x,
    split,
    {
      intro h_A,
      rw set.mem_Union₂,
      use [x, h_A],
      exact (h_f x h_A).2.1,
    },
    {
      intro h_u,
      rw set.mem_Union₂ at h_u,
      rcases h_u with ⟨a, h_a, h_x_mem⟩,
      have h_f_a_sbs := (h_f a h_a).2.2,
      exact set.mem_of_subset_of_mem h_f_a_sbs h_x_mem,
    },
  end,
  rw a_equals,
  apply is_open_Union,
  intro x,
end

[Matt Diamond]

I didn't complete the proof, but you can see the strategy at the end

[Matt Diamond]

by using apply, Lean will switch the goal to the function you need to prove, at which point you can intro the argument and apply the lemma again

[Matt Diamond]

the idea is to work in reverse

[Callum Cassidy-Nolan]

Ah I see what you're doing

[Callum Cassidy-Nolan]

This finishes it off:

import topology.basic

variables {X : Type} [topological_space X] {A: set X}

theorem munkres_13_1
  (h₀ : ∀ x ∈ A, ∃ U : set X, is_open U ∧ x ∈ U ∧ U ⊆ A)
  :
  is_open A
  :=
begin
  choose f h_f using h₀,
  have a_equals : A = ⋃ x h, f x h :=
  begin
    ext x,
    split,
    {
      intro h_A,
      rw set.mem_Union₂,
      use [x, h_A],
      exact (h_f x h_A).2.1,
    },
    {
      intro h_u,
      rw set.mem_Union₂ at h_u,
      rcases h_u with ⟨a, h_a, h_x_mem⟩,
      have h_f_a_sbs := (h_f a h_a).2.2,
      exact set.mem_of_subset_of_mem h_f_a_sbs h_x_mem,
    },
  end,
  rw a_equals,
  apply is_open_Union,
  intro x,
  apply is_open_Union,
  intro h_x,
  exact (h_f x h_x).1,
end

[Callum Cassidy-Nolan]

Thanks a lot Matt!

[Callum Cassidy-Nolan]

I'm still a little curious about defining helper variables and stuff mid way through proof though, do you usually use let or have?

[Matt Diamond]

it depends on what you're defining... have only retains the type of the variable, so if you're defining something where the actual definition matters, like a specific function or set, use let, but if you're just defining and proving a proposition, use have

[Kevin Buzzard]

let for things in the Type universe, have for things in the Prop universe

[Matt Diamond]

yep, what Kevin said