Theorem ZFSet.toSet_iUnion

Modification history

2025-11-21 11:20

Mathlib/SetTheory/ZFC/Basic.lean

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

Deleted ZFSet.toSet_iUnion View on Github →

2025-11-04 10:34

Mathlib/SetTheory/ZFC/Basic.lean

feat(SetTheory/ZFC): add `ZFSet.iUnion` (#30841) …

Added ZFSet.toSet_iUnion View on Github →