Topic: Equate Intersections
Ashvni Narayanan (Mar 24 2021 at 16:02):
I have proved that the intersection of finitely many clopens are clopen, and I have another set, which Lean infers as a possibly infinite intersection of clopens, which is actually the same as the previous set, hence is clopen. I am having trouble in showing that both the sets (given in
g and the goal) are indeed the same. This essentially involves splitting up elements of
↥(↑t ∩ Uᶜ), however, that is problematic. When I try to use
set.mem_inter_iff, I get the error :
rewrite tactic failed, motive is not type correct
λ (_a : Prop), h ↑i _ = h ↑i _.
I have no idea as to how to proceed, any help is appreciated, thank you!
Kevin Buzzard (Mar 24 2021 at 18:01):
It seems to me that if you can change
⋂ (i : H) (i_1 : i ∈ t) (i_1 : i ∈ Uᶜ), ... to
⋂ (i : H) (i_1 : i ∈ t \cap Uᶜ), ... then your life would be much easier :-) I'm fiddling with this now.
Ashvni Narayanan (Mar 24 2021 at 18:06):
I just managed to complete the proof! I found a way out :)
Kevin Buzzard (Mar 24 2021 at 18:06):
You might find life easier if you didn't have two things called
h and two things called
Kevin Buzzard (Mar 24 2021 at 19:19):
example (X Y : Type) (s t : set X) (F : X → set Y) : (⋂ (x : X) (h1 : x ∈ s) (h2 : x ∈ t), F x) = ⋂ (x : X) (h : x ∈ s ∩ t), F x := begin ext y, simp, end
by the way
Last updated: May 09 2021 at 10:11 UTC