Commit 2024-12-15 00:11 86f77dba

View on Github →

feat(SetTheory/ZFC/Basic): x ∈ y → ¬ y ⊆ x (#19967)

Estimated changes

added theorem PSet.not_mem_of_subset
added theorem PSet.not_subset_of_mem