Set coercion

Stream: Is there code for X?

[Pedro Minicz]

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]

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]

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]

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

[Kenny Lau]

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]

Here is a link to the stream I mentioned:

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

[Patrick Massot]

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

[Dan Stanescu]

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