Theorem ZFSet.toSet_sep

Modification history

2025-11-21 11:20

Mathlib/SetTheory/ZFC/Basic.lean

refactor(SetTheory/ZFC): deduplicate coercion to sets (#31287) …

Deleted ZFSet.toSet_sep View on Github →

2023-04-06 22:39

Mathlib/SetTheory/Zfc/Basic.lean

feat: port SetTheory.ZFC.Basic (#3165) …

Added ZFSet.toSet_sep View on Github →