Commit 2022-07-17 19:11 98f747f8

View on Github →

chore(set_theory/zfc): better def-eqs (#15210) We sidestep the equation compiler when not strictly needed, thus improving the definitional equalities on some basic definitions. This also allows us to inline many instances.

Estimated changes

Modified src/set_theory/zfc.lean

deleted def Set.empty

deleted def Set.mem

modified def pSet.Union

modified def pSet.image

deleted def pSet.mem

added theorem pSet.mk_func

added theorem pSet.mk_type

modified def pSet.powerset

modified def pSet.type