Stream: Is there code for X?

Topic: Set coercion

Pedro Minicz (Aug 17 2020 at 18:45):

Is the a coercion from set s to set α where s : set α in mathlib?

variables {α : Type} {s : set α} [decidable_pred s]

def set_coe : set s → set α :=
λ t x, if hx : x ∈ s then t ⟨x, hx⟩ else false


Dan Stanescu (Aug 17 2020 at 19:52):

Is this what you mean? This was mentioned in an earlier thread and there may be some other way:

variable A : set s
#check A
#check subtype.val '' A


Kenny Lau (Aug 17 2020 at 19:55):

might I point out that (a) it is not preferable to unfold set as a function to Prop, and (b) it is also not preferable to use if then else to define a Prop:

import data.set.basic

variables {α : Type} {s : set α}

def set_coe (t : set s) : set α :=
{ x | ∃ hx, (⟨x, hx⟩ : s) ∈ t }


Kenny Lau (Aug 17 2020 at 19:56):

(oh, right, and your code isn't #mwe because there is no coercion of s to a type without the import)

Kenny Lau (Aug 17 2020 at 19:57):

my code is only meant to be a version of your code that adheres more to mathlib guidelines, but as @Dan Stanescu points out, subtype.val '' A is more preferable.

Dan Stanescu (Aug 17 2020 at 20:01):

Here is a link to the stream I mentioned:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Subset.20of.20subset

Patrick Massot (Aug 17 2020 at 20:15):

subtype.val is often not the preferred way to express thing, you should probably use coe : s -> alpha

Dan Stanescu (Aug 17 2020 at 20:18):

Yes, that is mentioned in the thread I pointed to.

Last updated: May 16 2021 at 05:21 UTC