Zulip Chat Archive

Stream: new members

Topic: exists within an expression


view this post on Zulip Calle Sönne (Dec 09 2020 at 21:55):

I want to use the following theorem (the right implication):

lemma connected_space_iff_connected_component :
  connected_space α   x : α, connected_component x = univ :=

To a goal of the form:

connected_component x = s

where s : set \alpha.
Now just trying to apply this to my goal doesnt work, because there is an exists on the right hand expression. How do I unfold this "in" my apply statement? I am looking to do something like this:

apply connected_space_iff_connected_component.1 _ (exists.intro x)

which doesnt work.

view this post on Zulip Calle Sönne (Dec 09 2020 at 21:56):

So if I was not being clear, I already have a fixed x such that my goal is of the form connected_component x = s

view this post on Zulip Adam Topaz (Dec 09 2020 at 21:58):

You need to provide lean a proof h of connected_space \a, then do rcases on connected_space_iff_connected_component.mp h

view this post on Zulip Adam Topaz (Dec 09 2020 at 21:59):

This will provide you with a new x and a proof that its connected component is univ.

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:00):

It would be easier if you can provide a #mwe

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:01):

Okay here is the actual theorem that I am proving:

lemma connected_component_inter {α : Type*} [topological_space α] [t2_space α] [compact_space α] :
   x : α, connected_component x =  (Z : set α) (h : is_clopen Z), Z :=
begin
  intro x,
  apply connected_space_iff_connected_component.1 _ (exists.intro x),
end

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:01):

Adam Topaz said:

You need to provide lean a proof h of connected_space \a, then do rcases on connected_space_iff_connected_component.mp h

Ah, I was hoping to avoid this

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:03):

pro tip: If you use ```lean that will highlight the syntax properly

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:04):

I'm not sure how you expect to apply this lemma anyway. You don't know that your space is connected...

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:04):

Adam Topaz said:

pro tip: If you use ```lean that will highlight the syntax properly

Used ```clean :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (Dec 09 2020 at 22:05):

which oddly enough has some familial relationship to lean

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:06):

Adam Topaz said:

I'm not sure how you expect to apply this lemma anyway. You don't know that your space is connected...

I actually dont know why I thought of this

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:06):

I was working on a different method and then suddenly got this idea of how I thought I could shorten the proof considerably

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:06):

I mean... if the following is what you wanted to do, then I hope it helps :)

import topology.separation



lemma connected_component_inter {α : Type*} [topological_space α] [t2_space α] [compact_space α] :
   x : α, connected_component x =  (Z : set α) (h : is_clopen Z), Z :=
begin
  intro x,
  have : connected_space (connected_component x), sorry,
  rcases connected_space_iff_connected_component.1 this with y,hy⟩,
  sorry,
end

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:06):

not sure what that idea was

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:08):

Adam Topaz said:

I mean... if the following is what you wanted to do, then I hope it helps :)

import topology.separation



lemma connected_component_inter {α : Type*} [topological_space α] [t2_space α] [compact_space α] :
   x : α, connected_component x =  (Z : set α) (h : is_clopen Z), Z :=
begin
  intro x,
  have : connected_space (connected_component x), sorry,
  rcases connected_space_iff_connected_component.1 this with y,hy⟩,
  sorry,
end

Yes this is what I wanted to do, thanks. (but I dont remember my idea of the proof anymore :grinning_face_with_smiling_eyes: )

view this post on Zulip Kenny Lau (Dec 09 2020 at 22:10):

the RHS doesn't mention x

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:11):

Yeah this lemma can't be true

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:11):

You want to assume x is in the Z.

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:12):

Adam Topaz said:

You want to assume x is in the Z.

oh yes of course. This is the lemma https://stacks.math.columbia.edu/tag/08ZN

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:19):

Also is there some type of notation I can use to switch between considering a term of set α to a term of set s for some subset s (assuming it is a subset of s)? Like some sort of a lift?

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:20):

This is actually annoying to do...

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:20):

You have to use images and preimages w.r.t. the inclusion s \to \alpha.

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:22):

Note that therer is a coercion from s to \alphaso it's preferred to refer to this inclusion as coe (possibly with an accompanying type ascription).

view this post on Zulip Kenny Lau (Dec 09 2020 at 22:25):

@Calle Sönne you have reached the forbidden grounds of Lean territory

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:41):

Adam Topaz said:

You have to use images and preimages w.r.t. the inclusion s \to \alpha.

How do I get this inclusion? I can only figure out how to get the inclusion to set.univ (using set.inclusion)

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:43):

wait. Maybe thats right, I get this error:

type mismatch at application
  has_inter.inter t
term
  t
has type
  set α
but is expected to have type
  set set.univ
state:
α : Type u_1,
_inst_2 : topological_space α,
s t : set α,
h : is_clopen s,
h1 : is_preconnected t,
h2 : (s  t).nonempty,
v : set α := s
 t  s = t
All Messages (18)

From this code:

theorem preconnected_subset_clopen {α : Type*} [topological_space α] {s t : set α} (h : is_clopen s) (h1 : is_preconnected t) :
  (s  t).nonempty  t  s :=
begin
  intro h2,
  let v := s,
  apply subset_of_inter_eq_self_left,
  let u := ((set.inclusion (set.subset_univ t)) ⁻¹' (t  s)),
end

view this post on Zulip Calle Sönne (Dec 09 2020 at 22:48):

But is there really no easier way to talk about t ∩ s as a term of set t? :thinking:. Maybe I am going about the problem the wrong way. The reason I want to consider it as a subset of t is so that I can apply:

theorem is_clopen_iff [preconnected_space α] {s : set α} : is_clopen s  s =   s = univ :=

view this post on Zulip Adam Topaz (Dec 09 2020 at 22:52):

If you want to get t \cap s as a set in s, just use (coe : s \to \a) \inv ' t (i.e. the prreimage of t under the coercion from s to \alpha). (Sorry for the bad typesetting... don't have lean open right now)


Last updated: May 08 2021 at 19:11 UTC