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.)