Theorem ZFSet.coe_singleton

Modification history

2025-11-21 11:20

Mathlib/SetTheory/ZFC/Basic.lean

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

Added ZFSet.coe_singleton View on Github →