Zulip Chat Archive
Stream: new members
Topic: lifting "down"
Calle Sönne (Jan 18 2020 at 17:00):
How do I, as opposed to ulift, lift "down" a type? In my case I have an element in a set of sets and I want to treat it as a set.
Kenny Lau (Jan 18 2020 at 17:04):
you can't; that's the whole point
Kenny Lau (Jan 18 2020 at 17:04):
but an element in a set of sets can definitely be treated as a set (MWE?)
Calle Sönne (Jan 18 2020 at 17:09):
MWE?
Reid Barton (Jan 18 2020 at 17:09):
An element in a set of sets is a set
Kenny Lau (Jan 18 2020 at 17:10):
MWE = minimal working example
Reid Barton (Jan 18 2020 at 17:10):
I think you should explain your question in Lean and not English
Calle Sönne (Jan 18 2020 at 17:12):
lemma MWE (α : Type*) (opens : set (set α)) (U : opens) (T : set α) : U = T:=
Calle Sönne (Jan 18 2020 at 17:12):
Maybe it is my instinct to want to lift down as opposed to up
Calle Sönne (Jan 18 2020 at 17:13):
the MWE gives an error
Kenny Lau (Jan 18 2020 at 17:14):
U.1
Calle Sönne (Jan 18 2020 at 17:14):
and my question is how do I resolve this
Kenny Lau (Jan 18 2020 at 17:14):
it's not ulift
Calle Sönne (Jan 18 2020 at 17:16):
wait what does .1 do in this case?
Calle Sönne (Jan 18 2020 at 17:16):
Usually when I use it it is to access the carrier of some structure
Calle Sönne (Jan 18 2020 at 17:16):
but set is defined as a function
Kenny Lau (Jan 18 2020 at 17:18):
the way you coerce opens to a type is to use subtype
Kenny Lau (Jan 18 2020 at 17:18):
opens is not a type
Calle Sönne (Jan 18 2020 at 17:19):
oh
Last updated: Dec 20 2023 at 11:08 UTC