Intersectivity

📁 Source: Mathlib/MeasureTheory/Function/Intersectivity.lean

Statistics

Metric	Count
Definitions	0
Theorems bergelson, bergelson'	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bergelson 📖	mathematical	MeasurableSet ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike	Set Set.Infinite ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike Set.iInter Set.instMembership	—	bergelson' Set.Infinite.image Function.Injective.injOn Function.Embedding.injective LT.lt.trans_le Set.preimage_subset_of_surjOn Set.Finite.preimage MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.subset_iInter₂ Set.iInter₂_subset
bergelson' 📖	mathematical	MeasurableSet ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike	Set Set.Infinite ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike Set.iInter Set.instMembership	—	MeasureTheory.measure_iUnion_null MeasureTheory.Measure.instOuterMeasureClass Finset.countable instCountableNat MeasureTheory.meas_eLpNormEssSup_lt ENNReal.instCanonicallyOrderedAdd Set.mem_iUnion Set.mem_setOf Set.indicator_of_mem MeasureTheory.eLpNormEssSup_eq_zero_iff Set.indicator_ae_eq_zero Function.support_one NeZero.charZero_one RCLike.charZero_rclike Set.inter_univ nnnorm_one NormedDivisionRing.to_normOneClass IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero Finset.sum_apply Measurable.const_smul MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ Finset.measurable_sum_apply ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Measurable.fun_comp Measurable.indicator measurable_one Measurable.snd measurable_id' ENNReal.div_eq_inv_mul ENNReal.div_le_iff_le_mul Nat.cast_ne_zero one_ne_zero mul_comm nsmul_eq_mul Finset.card_range Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Set.indicator_le le_rfl MeasureTheory.lintegral_const_mul Finset.measurable_fun_sum MeasureTheory.lintegral_finset_sum Finset.sum_congr MeasureTheory.lintegral_indicator_one ENNReal.le_div_iff_mul_le Nat.cast_add Nat.cast_one Unique.instSubsingleton Nat.instNoMaxOrder nsmul_eq_mul' Finset.card_nsmul_le_sum le_bot_iff MeasureTheory.lintegral_one MeasureTheory.lintegral_mono Filter.limsup_le_of_le bot_le Filter.Eventually.of_forall MeasureTheory.exists_notMem_null_laverage_le ne_top_of_le_ne_top MeasureTheory.measure_ne_top Filter.le_limsup_of_le Filter.eventually_map eq_zero_or_neZero MeasureTheory.laverage_zero_measure MeasureTheory.laverage_const Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LE.le.trans ENNReal.div_le_div_right MeasureTheory.laverage_eq MeasureTheory.limsup_lintegral_le MeasureTheory.ae_of_all MeasureTheory.lintegral_const one_mul ENNReal.div_ne_zero eq_bot_mono Filter.Tendsto.limsup_eq ENNReal.instOrderTopology tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds bot_eq_zero' MulZeroClass.zero_mul ENNReal.Tendsto.mul_const Filter.Tendsto.comp ENNReal.tendsto_inv_nat_nhds_zero Filter.tendsto_add_atTop_nat ENNReal.natCast_ne_top mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid Set.indicator_apply Finset.sum_boole Finset.card_le_card Set.Finite.mem_toFinset Finset.mem_filter Set.iInter_congr_Prop Set.mem_iInter₂

---

← Back to Index