Commit 2022-05-02 02:37 922717e8
View on Github →chore(logic/function/basic): don't unfold set in cantor (#13822)
This uses set_of and mem consistently instead of using application everywhere, since f has type A -> set A instead of A -> A -> Prop. (Arguably, it could just be stated for A -> A -> Prop instead though.)