Mathlib Changelog
v4
Changelog
About
Github
Theorem
Set.mulIndicator_le_mulIndicator_apply_of_subset
Modification history
2024-10-07 17:59
Mathlib/Algebra/Order/Group/Indicator.lean
feat: supremum of directed indicators (#17467) …
Added
Set.mulIndicator_le_mulIndicator_apply_of_subset
View on Github →