basic): nonempty predicate (#15546)

Commit

3 years ago

feat(set_theory/zfc/basic): nonempty predicate (#15546) We define `Set.nonempty` matching `set.nonempty` and prove the basic results.

Author

vihdzp

Parents