Commit 2024-09-30 21:32 37814caf

View on Github →

feat(SetTheory/ZFC/Basic): make sInter computable (#17248) Moved from #15624 with permission from the original author. Co-authored by: RustyYato rustyyato@gmail.com

Estimated changes

added def ZFSet.sInter
modified theorem ZFSet.sInter_empty
added theorem ZFSet.sep_empty