## Stream: new members

### Topic: Working with choose!

#### Callum Cassidy-Nolan (Sep 21 2022 at 00:20):

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

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 (Sep 21 2022 at 01:02):

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

#### Matt Diamond (Sep 21 2022 at 01:11):

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

#### Matt Diamond (Sep 21 2022 at 01:36):

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 (Sep 21 2022 at 01:38):

you should just be able to use union lemmas twice

#### Mario Carneiro (Sep 21 2022 at 01:38):

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 (Sep 21 2022 at 01:41):

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 (Sep 21 2022 at 02:27):

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 (Sep 21 2022 at 02:37):

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 (Sep 21 2022 at 02:58):

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

hmm

#### Matt Diamond (Sep 21 2022 at 03:11):

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

#### Matt Diamond (Sep 21 2022 at 03:13):

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

#### Callum Cassidy-Nolan (Sep 21 2022 at 03:15):

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 (Sep 21 2022 at 03:19):

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 (Sep 21 2022 at 03:22):

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 (Sep 21 2022 at 03:24):

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 (Sep 21 2022 at 03:27):

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 (Sep 21 2022 at 03:29):

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 (Sep 21 2022 at 03:32):

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 (Sep 21 2022 at 03:34):

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 (Sep 21 2022 at 03:34):

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

#### Matt Diamond (Sep 21 2022 at 03:36):

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 (Sep 21 2022 at 03:37):

the idea is to work in reverse

#### Callum Cassidy-Nolan (Sep 21 2022 at 03:37):

Ah I see what you're doing

#### Callum Cassidy-Nolan (Sep 21 2022 at 03:39):

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 (Sep 21 2022 at 03:40):

Thanks a lot Matt!

#### Callum Cassidy-Nolan (Sep 21 2022 at 03:41):

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 (Sep 21 2022 at 03:42):

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 (Sep 21 2022 at 03:42):

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

#### Matt Diamond (Sep 21 2022 at 03:42):

yep, what Kevin said

Last updated: Dec 20 2023 at 11:08 UTC