Theorem ZFSet.nonempty_coe

Modification history

2025-11-21 11:20

Mathlib/SetTheory/ZFC/Basic.lean

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

Added ZFSet.nonempty_coe View on Github →