extracting term from Union

Stream: new members

[Jason KY.]

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.]

I have tried to use cases on ht but that does not seem to work :/

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Yury G. Kudryashov]

BTW, we probably have this lemma in mathlib

[Jason KY.]

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.]

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]

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]

I'd use rfl instead of ht in rintros.

[Yury G. Kudryashov]

(if I had no bUnion lemma)

[Jason KY.]

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]

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]

  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.]

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]

It is a bit odd that f depends on H

[Mario Carneiro]

the bUnion theorems may not be expecting this

[Jason KY.]

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]

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]

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

[Jason KY.]

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]

is_open_iff_forall_mem_open

[Jason KY.]

Nono, I don't want to see it yet

[Mario Carneiro]

:)

[Yury G. Kudryashov]

You can also use is_open_Union twice.

[Yury G. Kudryashov]

BTW, try choose f hfo hf using h

[Jason KY.]

Yury G. Kudryashov said:

You can also use is_open_Union twice.

Nice! That's exactly it!