Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes