# Zulip Chat Archive

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

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

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

Adam Topaz said:

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

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

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

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

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

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

#### 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 `\alpha`

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

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)

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