Commit 2024-11-13 12:06 01ebbe11

View on Github →

refactor(SetTheory/ZFC/Basic): redefine Definable (#16398) This allows automatic synthesis using typeclasses, see ZFSet.map. The new definition is ZFSet.Definable. The old PSet.Definable has been deprecated.

Estimated changes

Modified Mathlib/SetTheory/ZFC/Basic.lean

added theorem ZFSet.Definable.out_equiv

added theorem ZFSet.Definable₁.mk_out

added theorem ZFSet.Definable₁.out_equiv

added theorem ZFSet.Definable₂.mk_out

added theorem ZFSet.Definable₂.out_equiv

modified theorem ZFSet.image.mk

modified def ZFSet.image

added def ZFSet.map

modified theorem ZFSet.map_fval

modified theorem ZFSet.map_isFunc

modified theorem ZFSet.map_unique

modified theorem ZFSet.mem_image

modified theorem ZFSet.mem_map

modified theorem ZFSet.toSet_image