Theorem ZFSet.Definable₁.out_equiv

Modification history

2024-11-13 12:06
Mathlib/SetTheory/ZFC/Basic.lean
refactor(SetTheory/ZFC/Basic): redefine `Definable` (#16398) …
Added ZFSet.Definable₁.out_equivView on Github →