# Zulip Chat Archive

## Stream: new members

### Topic: Why isn't there an existential here?

#### Callum Cassidy-Nolan (Feb 20 2022 at 20:50):

Can I get some help with this proof ?

```
import topology.basic
theorem open_set_for_each
(X : Type*)
[topological_space X]
(A : set X)
(h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A) :
is_open A :=
begin
have f : A → set X ,
{
intro a,
let x := h₀ a,
-- Trying to get my set U
},
-- have : A = ⋃ (i : A), f i :=
-- {
-- }
end
```

Pretty much I'm trying to build my function from `A`

to `set X`

by evaluating h0 at a point a, but I'm running into trouble because after `let x : = h0 a`

my goal state is

```
X: Type u_1
_inst_1: topological_space X
A: set X
h₀: ∀ (x : X), x ∈ A → (∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A)
a: ↥A
x: ↑a ∈ A → (∃ (U : set X), is_open U ∧ ↑a ∈ U ∧ U ⊂ A) := h₀ ↑a
⊢ set X
```

but I thought that x would have become `∃ (U : set X), is_open U ∧ ↑a ∈ U ∧ U ⊂ A`

and then I could use that set `U`

...

#### Patrick Massot (Feb 20 2022 at 20:57):

Did you try `suggest`

?

#### Patrick Massot (Feb 20 2022 at 21:00):

Also, you probably meant `⊆`

, not `⊂`

#### Patrick Massot (Feb 20 2022 at 21:01):

As suggest will reveal, your lemma is a repackaging of docs#is_open_iff_forall_mem_open

#### Patrick Massot (Feb 20 2022 at 21:01):

If you feel this is cheating then you'll have to tell us more about the constraints in your game.

#### Callum Cassidy-Nolan (Feb 20 2022 at 21:13):

My goal is to prove it using the fact that the union of open sets is still open

#### Callum Cassidy-Nolan (Feb 20 2022 at 21:14):

So first I want to build that function f which takes an element of `A`

and maps it to the `U`

you would get from `h0`

, then I'll take the union of that function over every `i`

in `A`

#### Callum Cassidy-Nolan (Feb 20 2022 at 21:15):

But the goal state isn't like I expected.

#### Ruben Van de Velde (Feb 20 2022 at 21:19):

You'll want `let f`

, not `have`

, in any case

#### Patrick Massot (Feb 20 2022 at 21:22):

The first line you want is probably `choose! f hf using h₀,`

then

#### Ruben Van de Velde (Feb 20 2022 at 21:23):

The problem you have seems to be related to the difference between sets and types in lean, though. I'd try `let x := h\0 a _,`

, leaving a proof obligation for a \in A, and then simp or suggest will probably prove that

#### Ruben Van de Velde (Feb 20 2022 at 21:24):

But Patrick's suggestion will likely get you more than one step ahead :)

#### Patrick Massot (Feb 20 2022 at 21:25):

Something like:

```
begin
choose! f hf using h₀,
have : A = ⋃ x ∈ A, f x,
{
sorry },
rw this,
apply is_open_bUnion,
sorry
end
```

#### Patrick Massot (Feb 20 2022 at 21:32):

I just read the code you actually pasted. There is no way you'll be able to construct data out of that existential without using choice. You can try and you'll get Lean complaining about only being able to eliminate into Prop.

#### Patrick Massot (Feb 20 2022 at 21:33):

You can try with

```
begin
let f : A → set X ,
{ intro a,
cases h₀ a a.property with U hU,
},
-- have : A = ⋃ (i : A), f i :=
-- {
-- }
end
```

#### Patrick Massot (Feb 20 2022 at 21:33):

And this introduces the subtype associated to `A`

, which you should avoid whenever possible. Note how my version features no function defined only on `A`

.

#### Callum Cassidy-Nolan (Feb 21 2022 at 00:30):

Thanks for showing me the `choose`

tactic, I managed to get the proof!

```
import topology.basic
open set
theorem open_set_for_each
(X : Type*)
[topological_space X]
(A : set X)
(h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊆ A) :
is_open A :=
begin
choose! f hf using h₀,
have : A = ⋃ x ∈ A, f x,
{
ext p,
split,
{
intro hp,
have hfp := hf p hp,
rw mem_Union,
use p,
rw mem_Union,
use hp,
exact hfp.2.1,
},
{
intro hp,
rw mem_Union at hp,
cases hp with i hi,
rw mem_Union at hi,
cases hi with hia hpfi,
have x := hf i hia,
exact x.2.2 hpfi,
}
},
rw this,
apply is_open_bUnion,
intros i hi,
exact (hf i hi).1,
end
```

#### Callum Cassidy-Nolan (Feb 21 2022 at 00:30):

Do you have any feedback to shorten the intermediate proof?

#### Yaël Dillies (Feb 21 2022 at 00:33):

You can use `mem_Union₂`

instead of `mem_Union`

twice.

#### Kyle Miller (Feb 21 2022 at 02:48):

Here's a way to avoid choice:

```
theorem open_set_for_each
(X : Type*)
[topological_space X]
(A : set X)
(h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊆ A) :
is_open A :=
begin
have : A = ⋃ U (h : U ⊆ A ∧ is_open U), U,
{ ext p,
simp only [mem_Union, exists_prop],
split,
{ intro hp,
rcases h₀ p hp with ⟨U, hU, hxU, hUA⟩,
use [U, hUA, hU, hxU], },
{ rintro ⟨U, ⟨hUA, hU⟩, hpU⟩,
exact hUA hpU, }, },
rw this,
apply is_open_bUnion,
rintros U ⟨hU, hU'⟩,
exact hU',
end
```

(If you're unfamiliar with docs#rintro and docs#rcases, they're ways to simplify strings of `cases`

.)

#### Kyle Miller (Feb 21 2022 at 03:39):

(This is actually somewhat similar in spirit to the choice-ful and choice-free proofs of Theorem 1.4 of Andrej Bauer's Five stages of accepting constructive mathematics.)

#### Callum Cassidy-Nolan (Feb 21 2022 at 12:56):

Thanks seeing that way is nice too

#### Patrick Massot (Feb 21 2022 at 12:57):

Yes, I wanted to create the function that was requested but the lemma itself doesn't need choice of course.

#### Callum Cassidy-Nolan (Feb 21 2022 at 12:58):

I moved on to a new question

I tried to model it like some of the theorems I saw in the docs, but I'ts not completely working out here's what I've gotten to so far

```
theorem intersection_of_topologies
(X : Type*)
(ι : Sort*)
[topological_space X]
(f : ι → topological_space X) :
topological_space ∩ x ∈ ι, f x :=
begin
sorry
end
```

Although I know parts of it aren't written correctly...

#### Patrick Massot (Feb 21 2022 at 12:59):

Your conclusion doesn't mean anything (and I would be surprised if Lean accepts to parse it)

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:00):

Yeah, I'm trying to figure out how to use this definition image.png

in the book, we're saying that this set (the intersection) is a topology on X. But I'm not quite sure how I would write that in terms of the type theory version...

#### Patrick Massot (Feb 21 2022 at 13:01):

```
import topology.basic
def intersection_of_topologies {X : Type*} {ι : Sort*}
(f : ι → topological_space X) : topological_space X :=
{ is_open := λ s, ∀ i, (f i).is_open s,
is_open_univ := sorry,
is_open_inter := sorry,
is_open_sUnion := sorry }
```

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:03):

Doesn't the statement we're proving have to talk about `f`

how could `topological_space X`

represent "the intersection of the topologies is a topology"?

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:06):

Wait with a goal of `topological_space X`

we're constructing a topology right?

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:07):

I'm still confused as to why we don't need to talk about the intersection in our goal though...

#### Patrick Massot (Feb 21 2022 at 13:23):

`topological_space X`

is the type of topologies on X. A term having this type gathers the data of which sets are open with the proofs of the conditions these opens sets must satisfy.

#### Patrick Massot (Feb 21 2022 at 13:24):

If you really want to see the intersection sign then you can write

```
def intersection_of_topologies {X : Type*} {ι : Sort*}
(f : ι → topological_space X) : topological_space X :=
{ is_open := λ s, s ∈ ⋂ i, {t | (f i).is_open t},
is_open_univ := sorry,
is_open_inter := sorry,
is_open_sUnion := sorry }
```

#### Patrick Massot (Feb 21 2022 at 13:26):

and then start each proof with `simp_rw [set.mem_Inter, set.mem_set_of_eq],`

to get back to my formulation.

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:35):

Is this definition a proof that the intersection of the topologies is a topology?

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:36):

I thought we would write `theorem`

instead?

#### Patrick Massot (Feb 21 2022 at 13:36):

`theorem`

would mean it has only proofs. Here we are combining data (is the first field) with proofs

#### Reid Barton (Feb 21 2022 at 13:38):

mathlib has no way to say that "`T : set (set X)`

is a topology on `X`

", other than by building a `topological_space`

structure whose first component is `T`

. In other words, there's no `is_topology`

.

#### Reid Barton (Feb 21 2022 at 13:38):

Nothing fundamental about that, we just never needed it.

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:39):

Ok, so we have no way of saying `is_topology`

, but so then how do we show something *is a topology*?

#### Reid Barton (Feb 21 2022 at 13:39):

As shown above

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:39):

So you make a definition?

#### Mauricio Collares (Feb 21 2022 at 13:41):

The three sorries in Patrick's example should be filled in with proofs that the family of open sets given in `is_open`

satisfies the correct axioms

#### Mauricio Collares (Feb 21 2022 at 13:41):

So it's a structure definition with one data field (component?) and three proof fields

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:43):

Ok, I think I'm understanding it a little better now, and this thing `is_open : set α → Prop`

is a function which determines if something is open or not right?

#### Patrick Massot (Feb 21 2022 at 13:44):

Yes.

#### Patrick Massot (Feb 21 2022 at 13:45):

But you don't have to use mathlib's way if you only want to do exercises in topology. Nothing prevents you from writing

```
import topology.basic
open set
structure is_topology {X : Type*} (T : set (set X)) : Prop :=
(univ_op : univ ∈ T)
(inter_op : ∀ u v ∈ T, u ∩ v ∈ T)
(Union_op : ∀ S : set (set X), S ⊆ T → ⋃₀ S ∈ T)
```

and playing with it. But you won't have all the lemmas we have about topologies in mathlib.

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:46):

So in our scenario our open sets are the ones which are open in all each of the topologies in the family, so that's why you're using `∀ i, (f i).is_open s`

right?

#### Patrick Massot (Feb 21 2022 at 13:46):

You don't even have to use precisely the same wording, you can use:

```
structure is_topology {X : Type*} (T : set (set X)) : Prop :=
(Inter_op : ∀ S : set (set X), S ⊆ T → finite S → ⋂₀ S ∈ T)
(Union_op : ∀ S : set (set X), S ⊆ T → ⋃₀ S ∈ T)
```

#### Julian Berman (Feb 21 2022 at 13:47):

Maybe glossary#bundled-vs-unbundled is briefly useful too

#### Callum Cassidy-Nolan (Feb 21 2022 at 13:48):

Thanks, I'm starting to understand this more - I had never done a proof like that yet so the examples help!

Last updated: Dec 20 2023 at 11:08 UTC