Theorem Set.isLowerSet_powerset

Modification history

2026-09-22 13:54
Mathlib/Data/Set/Sups.lean
feat(Data/Finset/Sups): add `infs_eq_inter` and `powerset_inter_eq_inter` (#42520) …
Added Set.isLowerSet_powersetView on Github →