Theorem Finset.isLowerSet_preimage_coe_powerset

Modification history

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