Theorem ZFSet.Definable₁.mk_out

Modification history

2024-11-13 12:06

Mathlib/SetTheory/ZFC/Basic.lean

refactor(SetTheory/ZFC/Basic): redefine `Definable` (#16398) …

Added ZFSet.Definable₁.mk_out View on Github →