Zulip Chat Archive

Stream: new members

Topic: extracting term from Union


view this post on Zulip 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?

view this post on Zulip Jason KY. (May 20 2020 at 20:37):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 20 2020 at 20:42):

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

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 20:44):

BTW, we probably have this lemma in mathlib

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 20:47):

I'd use rfl instead of ht in rintros.

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 20:47):

(if I had no bUnion lemma)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 20 2020 at 20:56):

It is a bit odd that f depends on H

view this post on Zulip Mario Carneiro (May 20 2020 at 20:57):

the bUnion theorems may not be expecting this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 20 2020 at 20:59):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 20 2020 at 21:01):

is_open_iff_forall_mem_open

view this post on Zulip Jason KY. (May 20 2020 at 21:01):

Nono, I don't want to see it yet

view this post on Zulip Mario Carneiro (May 20 2020 at 21:01):

:)

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 21:42):

You can also use is_open_Union twice.

view this post on Zulip Yury G. Kudryashov (May 20 2020 at 21:46):

BTW, try choose f hfo hf using h

view this post on Zulip 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