Theorem HasSubset.Subset.sdiff_ssubset_of_nonempty

Modification history

2026-07-06 15:50
Mathlib/Order/BooleanAlgebra/Set.lean
feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet`, `Class` (#32983) …
Deleted HasSubset.Subset.sdiff_ssubset_of_nonemptyView on Github →
2026-06-09 08:51
Mathlib/Order/BooleanAlgebra/Set.lean
chore: rename `diff` to `sdiff` (#40184) …
Added HasSubset.Subset.sdiff_ssubset_of_nonemptyView on Github →