filter subtype lift

Stream: maths

[Bernd Losert]

Say I have a filter F : filter (subtype s) where s : set α. I want to "lift" F to a filter α. What is the correct way to do this? I've been hacking it with coe but it does not work sometimes.

[Johan Commelin]

@Bernd Losert Is that F.map coe?

[Johan Commelin]

You can map a filter on α to a filter on β along any function f : α → β

[Bernd Losert]

Yes, I've been doing map coe F, but there are situations where it gets confused because it can't figure out which β to use.

[Heather Macbeth]

You can be more explicit with (coe : s → β)

[Bernd Losert]

Nice. That cleared the problem. Thank you.