Zulip Chat Archive

Stream: new members

Topic: Set membership and type judgements


view this post on Zulip Aniruddh Agarwal (May 22 2020 at 09:17):

Potentially dumb question. Are ex1 and ex2 below equivalent:

universe u

variable {α : Type u}

def P (a : α) (b : α) : Prop := sorry

def ex1 (S : set α) := { x : α |  y : α, y  S  P x y }
def ex2 (S : set α) := { x : α |  y  S, P x y }

view this post on Zulip Kenny Lau (May 22 2020 at 09:18):

yes, definitionally

view this post on Zulip Kevin Buzzard (May 22 2020 at 09:28):

You can check to see if rfl proves that they are equal

view this post on Zulip Aniruddh Agarwal (May 22 2020 at 09:31):

Good idea!


Last updated: May 10 2021 at 19:16 UTC