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

:)

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