Commit 2025-11-04 10:34 9217ddd1

View on Github →

feat(SetTheory/ZFC): add ZFSet.iUnion (#30841) which is just sUnion (range f). We add a new definition for it instead of making ⋃ i, f i a notation of sUnion (range f), because the simp normal form of (sUnion (range f)).toSet is not ⋃ i, (f i).toSet.

Estimated changes

added theorem ZFSet.mem_iUnion
modified theorem ZFSet.mem_range
modified theorem ZFSet.mem_range_self
added theorem ZFSet.subset_iUnion
added theorem ZFSet.toSet_iUnion
modified theorem ZFSet.toSet_range
added theorem ZFSet.rank_iUnion