Indicator

📁 Source: Mathlib/MeasureTheory/Integral/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_measure_of_ae_tendsto_indicator, tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure, tendsto_measure_of_tendsto_indicator, tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure	4
Total	4

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_measure_of_ae_tendsto_indicator 📖	mathematical	MeasurableSet Filter.Eventually Set Set.instHasSubset Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Filter.Tendsto ENNReal DFunLike.coe nhds ENNReal.instTopologicalSpace	—	Measure.instOuterMeasureClass lintegral_indicator_one tendsto_lintegral_filter_of_dominated_convergence Filter.Eventually.of_forall Measurable.indicator measurable_const Filter.mp_mem Filter.univ_mem' le_imp_le_of_le_of_le Set.indicator_le_indicator_apply_of_subset zero_le ENNReal.instCanonicallyOrderedAdd le_refl T5Space.toT1Space ENNReal.instT5Space NeZero.charZero_one ENNReal.instCharZero
tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure 📖	mathematical	MeasurableSet Filter.Eventually Set Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Filter.Tendsto ENNReal DFunLike.coe nhds ENNReal.instTopologicalSpace	—	Measure.instOuterMeasureClass tendsto_measure_of_ae_tendsto_indicator MeasurableSet.univ measure_ne_top Filter.Eventually.of_forall Set.subset_univ
tendsto_measure_of_tendsto_indicator 📖	mathematical	MeasurableSet Filter.Eventually Set Set.instHasSubset Set.instMembership	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike nhds ENNReal.instTopologicalSpace	—	Filter.eq_or_neBot Filter.tendsto_bot tendsto_measure_of_ae_tendsto_indicator measurableSet_of_tendsto_indicator ae_of_all Measure.instOuterMeasureClass
tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure 📖	mathematical	MeasurableSet Filter.Eventually Set Set.instMembership	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike nhds ENNReal.instTopologicalSpace	—	Filter.eq_or_neBot Filter.tendsto_bot tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure measurableSet_of_tendsto_indicator ae_of_all Measure.instOuterMeasureClass

---

← Back to Index