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: Dec 20 2023 at 11:08 UTC