Cast to superset

Stream: new members

[Eric Zhao]

Second day writing Lean; so I'm not even sure this is a well formed question. How can I get the universal set of some subtype B of A, but as a Set A?

[Kyle Miller]

If you have enough imports, this might work: ((Set.univ : Set B) : Set A). That inserts a coercion function, which is defined to be the image of the set through the function Subtype.val : B -> A.

[Ruben Van de Velde]

Is this your question?

import Mathlib

variable {A : Type*} {p : A → Prop}

def up : Set { x // p x } → Set A := sorry

[Eric Zhao]

Yes, for example I want something like

def z : Set ℕ := ((Set.univ : Set {n : ℕ // n < 4}) : Set ℕ)

Is this supposed to work automatically? It doesn't seem to

[Kyle Miller]

The secret is to use a Set coerced to a type rather than a Subtype directly.

def z : Set ℕ := ((Set.univ : Set {n : ℕ | n < 4}) : Set ℕ)

[Kyle Miller]

These are fundamentally the same, but syntactically different, and this coercion is only defined for this case. It's possible to define one for Subtype if you need it.

[Kyle Miller]

The coercion is defined at docs#Set.instCoeHeadSetElem

[Eric Zhao]

Oh I see. Though in my case I already have a subtype that I'd like to use. How would I go about defining the coercion for it?

[Eric Zhao]

Oh, it seems to go through by invoking Subtype.val '' ...?

[Eric Zhao]

To check my understanding: we're projecting out the value for each element of the set (which are of the subtype B) back to the type A

[Eric Zhao]

@Kyle Miller Thank you!