# Zulip Chat Archive

## 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

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

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