Theorem tendsto_indicator_bUnion_finset

Modification history

2023-02-12 15:02
Mathlib/Order/Filter/IndicatorFunction.lean
chore: tidy various files (#2236)
Deleted tendsto_indicator_bUnion_finsetView on Github →
2023-01-24 20:43
Mathlib/Order/Filter/IndicatorFunction.lean
feat: port Order.Filter.IndicatorFunction (#1821)
Added tendsto_indicator_bUnion_finsetView on Github →