# Zulip Chat Archive

## Stream: new members

### Topic: extracting term from Union

#### Jason KY. (May 20 2020 at 20:36):

Hi,

I am currently trying to prove somethings about topological spaces and

have the following #mwe

```
import topology.basic
variables {X : Type*} [topological_space X]
lemma open_of_has_smaller {U : set X}
(h : ∀ x ∈ U, ∃ (Nₓ : set X) (h₀ : is_open Nₓ), x ∈ Nₓ ∧ Nₓ ⊆ U) :
is_open U :=
begin
-- So what I want to do is use ⋃ (x ∈ U) Nₓ
choose f hf using h,
have : is_open ⋃ (x ∈ U), f x H,
refine is_open_sUnion _,
rintros t ⟨x, ht⟩,
-- How do I extract x ∈ U from (λ (x : X), ⋃ (H : x ∈ U), f x H) x = t
sorry
end
```

As indicated, how do I extract `x ∈ U`

from `(λ (x : X), ⋃ (H : x ∈ U), f x H) x = t`

?

#### Jason KY. (May 20 2020 at 20:37):

I have tried to use cases on `ht`

but that does not seem to work :/

#### Yury G. Kudryashov (May 20 2020 at 20:42):

I wish zulip Android app used a don't work better Unicode man coverage. Or had an option to choose the font.

#### Reid Barton (May 20 2020 at 20:42):

`is_open_sUnion`

isn't the right lemma to use. You want `is_open_bUnion`

.

#### Yury G. Kudryashov (May 20 2020 at 20:44):

BTW, we probably have this lemma in mathlib

#### Jason KY. (May 20 2020 at 20:45):

Yury G. Kudryashov said:

BTW, we probably have this lemma in mathlib

I'm currently formalising some lecture notes as a learning experience!

#### Jason KY. (May 20 2020 at 20:45):

Reid Barton said:

`is_open_sUnion`

isn't the right lemma to use. You want`is_open_bUnion`

.

Alright, I'll try to use this instead

#### Alex J. Best (May 20 2020 at 20:46):

If I saw `(λ (x : X), ⋃ (H : x ∈ U), f x H) x = t`

I'd dsimp it immediately, but in this case that removes all mention of H.

#### Yury G. Kudryashov (May 20 2020 at 20:47):

I'd use rfl instead of ht in rintros.

#### Yury G. Kudryashov (May 20 2020 at 20:47):

(if I had no bUnion lemma)

#### Jason KY. (May 20 2020 at 20:50):

emm, using rfl will give me `is_open ((λ (x : X), ⋃ (H : x ∈ U), f x H) x)`

which I don't think I can prove since I can't use sUnion on this

#### Mario Carneiro (May 20 2020 at 20:54):

You should try to avoid unions over propositions like this, by using `bUnion`

theorems, but you can use `Union`

if they come up

#### Mario Carneiro (May 20 2020 at 20:55):

```
have : is_open ⋃ (x ∈ U), f x H,
refine is_open_sUnion _,
```

This is a wrong move, `⋃ (x ∈ U), f x H`

is a bUnion not an sUnion

#### Jason KY. (May 20 2020 at 20:56):

I'm currently trying to use `is_open_bUnion`

but can't seem to get it to work. I think the way I defined `f`

is wrong

#### Mario Carneiro (May 20 2020 at 20:56):

It is a bit odd that `f`

depends on `H`

#### Mario Carneiro (May 20 2020 at 20:57):

the bUnion theorems may not be expecting this

#### Jason KY. (May 20 2020 at 20:58):

right, I'm thinking iere is a way to swap the type of `f`

so `f`

will have type `somthing not dependent on x \all(x : X), → set X`

instead of `Π (x : X), x ∈ U → set X`

#### Mario Carneiro (May 20 2020 at 20:58):

anyway there is no need to use choice in the theorem, you can prove that U is the union of all its open subsets

#### Mario Carneiro (May 20 2020 at 20:59):

I'm also pretty sure there is already a theorem stating approximately this in mathlib

#### Jason KY. (May 20 2020 at 21:00):

Alright, I'll try your approach for now and if that doesn't go well I can cheat a bit by looking in mathlib

#### Mario Carneiro (May 20 2020 at 21:01):

`is_open_iff_forall_mem_open`

#### Jason KY. (May 20 2020 at 21:01):

Nono, I don't want to see it yet

#### Mario Carneiro (May 20 2020 at 21:01):

:)

#### Yury G. Kudryashov (May 20 2020 at 21:42):

You can also use `is_open_Union`

twice.

#### Yury G. Kudryashov (May 20 2020 at 21:46):

BTW, try `choose f hfo hf using h`

#### Jason KY. (May 20 2020 at 21:46):

Yury G. Kudryashov said:

You can also use

`is_open_Union`

twice.

Nice! That's exactly it!

Last updated: May 13 2021 at 23:16 UTC