set.preimage notation trouble

Stream: general

[Kevin Buzzard]

import data.set.basic

example (X Y : Type) (f : X → Y) (S : set (set Y)) : set (set X) :=
--(f⁻¹')'' S -- doesn't work
-- set.image (set.preimage f) S -- works
-- (set.preimage f) '' S -- works
sorry

I can't get the set.preimage notation to work with this set-up, even with type ascriptions: set.image ((f⁻¹') : (set Y → set X)) S doesn't work for me. What am I doing wrong?

[Mario Carneiro]

This just came up with the conversation about sections. Use (⁻¹') f '' S

[Mario Carneiro]

although I personally find set.preimage f '' S easier to follow

[Patrick Massot]

and even easier with parentheses

[Mario Carneiro]

I guess I'm used to application having higher precedence than binary operators :shrug: