exists within an expression

Stream: new members

[Calle Sönne]

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]

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]

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]

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

[Adam Topaz]

It would be easier if you can provide a #mwe

[Calle Sönne]

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]

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]

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

[Adam Topaz]

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

[Calle Sönne]

Adam Topaz said:

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

Used ```clean :grinning_face_with_smiling_eyes:

[Reid Barton]

which oddly enough has some familial relationship to lean

[Calle Sönne]

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]

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]

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]

not sure what that idea was

[Calle Sönne]

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]

the RHS doesn't mention x

[Adam Topaz]

Yeah this lemma can't be true

[Adam Topaz]

You want to assume x is in the Z.

[Calle Sönne]

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]

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]

This is actually annoying to do...

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Calle Sönne]

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]

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]

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]

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)