## Stream: new members

### Topic: exists within an expression

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

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

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

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

#### Adam Topaz (Dec 09 2020 at 22:00):

It would be easier if you can provide a #mwe

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


#### Calle Sönne (Dec 09 2020 at 22:01):

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

#### Adam Topaz (Dec 09 2020 at 22:03):

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

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

#### Calle Sönne (Dec 09 2020 at 22:04):

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

Used clean :grinning_face_with_smiling_eyes:

#### Reid Barton (Dec 09 2020 at 22:05):

which oddly enough has some familial relationship to lean

#### Calle Sönne (Dec 09 2020 at 22:06):

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

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

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


#### Calle Sönne (Dec 09 2020 at 22:06):

not sure what that idea was

#### Calle Sönne (Dec 09 2020 at 22:08):

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: )

#### Kenny Lau (Dec 09 2020 at 22:10):

the RHS doesn't mention x

#### Adam Topaz (Dec 09 2020 at 22:11):

Yeah this lemma can't be true

#### Adam Topaz (Dec 09 2020 at 22:11):

You want to assume x is in the Z.

#### Calle Sönne (Dec 09 2020 at 22:12):

You want to assume x is in the Z.

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

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

#### Adam Topaz (Dec 09 2020 at 22:20):

This is actually annoying to do...

#### Adam Topaz (Dec 09 2020 at 22:20):

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

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

#### Kenny Lau (Dec 09 2020 at 22:25):

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

#### Calle Sönne (Dec 09 2020 at 22:41):

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)

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


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


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