Commit 2024-10-07 17:59 847ce656

View on Github →

feat: supremum of directed indicators (#17467) ... is indicator of the suprema From GibbsMeasure

Estimated changes

Modified Mathlib/Algebra/Order/Group/Indicator.lean

added theorem Set.iSup_mulIndicator

added theorem Set.mulIndicator_le_mulIndicator_apply_of_subset

modified theorem Set.mulIndicator_le_mulIndicator_of_subset

added theorem Set.mulIndicator_mono