Commit 2025-05-09 16:12 f508a8e4

View on Github →

feat(SetTheory/ZFC/Basic): order instances (#19946) Sets form a partial order under the subset relation.

Estimated changes

added theorem ZFSet.le_def
added theorem ZFSet.lt_def
added theorem PSet.le_def
added theorem PSet.lt_def