Commit 2023-01-24 20:43 66724c37

View on Github →

feat: port Order.Filter.IndicatorFunction (#1821)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/IndicatorFunction.lean

added theorem Antitone.tendsto_indicator

added theorem Filter.EventuallyEq.indicator

added theorem Filter.EventuallyEq.indicator_zero

added theorem Filter.EventuallyEq.support

added theorem Monotone.tendsto_indicator

added theorem indicator_eventuallyEq

added theorem indicator_eventuallyLe_indicator

added theorem indicator_union_eventuallyEq

added theorem tendsto_indicator_bUnion_finset