Restricting a function all the way

Stream: new members

[Abdullah Uyu]

I have a function f: X → X → Prop that I can restrict to f' : myset → X → Prop. How can I restrict it further and get a function f'' : myset → myset → Prop:

import Mathlib.Data.Set.Function

open Set

variable (X : Type) (f : X → X → Prop) (myset : Set X)

def f' : myset → X → Prop := myset.restrict f

[Abdullah Uyu]

I guess I can write

def f'' :
    myset → myset → Prop :=
  fun a b : myset => myset.restrict (myset.restrict f a) b

Can I make this shorter? My original f actually is of type X → X → X → Prop, so I have to apply the restrict three times and it'll become very hard to read.

[Paul Rowe]

I think you're getting into trouble with your variables. If you check the type of f', you'll see that it takes all three of your variable types before accepting an argument of type myset. So you could write

def f'' : myset → myset → Prop := fun x => myset.restrict (f' X f myset x)

But I'm guessing you don't intend for those to be arguments to f' (and might not be in your real work)`. So you might be able to get away with

def f'' : myset → myset → Prop := fun  x => myset.restrict (f' x)

in your real code.