Commit 2023-06-28 10:21 682b2572

View on Github →

feat: add lemmas about Filters and Set.indicator (#5240)

Add multiplicative versions of all lemmas in Order.Filter.IndicatorFunction.
Add several new lemmas.

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Antitone.piecewise_eventually_eq_iInter

added theorem Monotone.piecewise_eventually_eq_iUnion

Modified Mathlib/Order/Filter/IndicatorFunction.lean

added theorem Antitone.mulIndicator_eventuallyEq_iInter

deleted theorem Antitone.tendsto_indicator

added theorem Antitone.tendsto_mulIndicator

deleted theorem Filter.EventuallyEq.indicator

deleted theorem Filter.EventuallyEq.indicator_zero

added theorem Filter.EventuallyEq.mulIndicator_one

added theorem Filter.EventuallyEq.of_mulIndicator

added theorem Filter.EventuallyEq.of_mulIndicator_const

deleted theorem Filter.EventuallyEq.support

added theorem Monotone.mulIndicator_eventuallyEq_iUnion

deleted theorem Monotone.tendsto_indicator

added theorem Monotone.tendsto_mulIndicator

deleted theorem indicator_eventuallyEq

deleted theorem indicator_eventuallyLE_indicator

deleted theorem indicator_union_eventuallyEq

added theorem mulIndicator_biUnion_finset_eventuallyEq

added theorem mulIndicator_eventuallyEq

added theorem mulIndicator_eventuallyLE_mulIndicator

added theorem mulIndicator_union_eventuallyEq

deleted theorem tendsto_indicator_biUnion_finset

added theorem tendsto_mulIndicator_biUnion_finset