Count

📁 Source: Mathlib/MeasureTheory/Measure/Count.lean

Statistics

Metric	Count
Definitions count	1
Theorems map_count_le, ae_count_iff, instSigmaFinite, isFiniteMeasure, count_apply, count_apply_eq_top, count_apply_eq_top', count_apply_finite, count_apply_finite', count_apply_finset, count_apply_finset', count_apply_infinite, count_apply_lt_top, count_apply_lt_top', count_eq_zero_iff, count_injective_image, count_injective_image', count_ne_zero, count_ne_zero'', count_ne_zero_iff, count_singleton, count_singleton', count_univ, le_count_apply, count_real_singleton, count_real_singleton', count_eq_dirac, count_eq_dirac	28
Total	29

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_count_le 📖	mathematical	Measurable	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder MeasureTheory.Measure.map MeasureTheory.Measure.count	—	MeasureTheory.Measure.le_intro MeasureTheory.Measure.map_apply MeasureTheory.Measure.count_apply MeasurableSet.preimage encard_image Set.image_preimage_subset Set.encard_le_encard

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_real_singleton 📖	mathematical	—	Measure.real Measure.count Set Set.instSingletonSet Real Real.instOne	—	count_real_singleton' MeasurableSingletonClass.measurableSet_singleton
count_real_singleton' 📖	mathematical	MeasurableSet Set Set.instSingletonSet	Measure.real Measure.count Set Set.instSingletonSet Real Real.instOne	—	measureReal_def Measure.count_singleton' ENNReal.toReal_one

MeasureTheory.Measure

Definitions

Name	Category	Theorems
count 📖	CompOp	51 math math: count.instSigmaFinite, MeasureTheory.hasFiniteIntegral_count_iff_enorm, count_injective_image', count.isFiniteMeasure, count_apply, count_singleton', NNReal.count_const_le_le_of_tsum_le, MeasureTheory.eLpNorm_count_lt_top_of_lt, count_apply_eq_top, Subsingleton.count_eq_dirac, count_eq_zero_iff, instIsMulLeftInvariantCount, essInf_count, Function.Injective.map_count_le, count_apply_lt_top, instIsAddLeftInvariantCount, MeasureTheory.lintegral_count, count_singleton, instIsInvInvariantCount, MeasureTheory.count_withDensity, count_apply_finset', MeasureTheory.count_withDensity', MeasureTheory.count_real_singleton', ENNReal.count_const_le_le_of_tsum_le, count_apply_infinite, instIsAddRightInvariantCount, Unique.count_eq_dirac, ae_count_iff, essSup_count_eq_ciSup, count_apply_finset, count_univ, MeasureTheory.lintegral_count', ProbabilityTheory.uniformOn_univ, MeasureTheory.eLpNormEssSup_count, le_count_apply, essSup_count, MeasureTheory.eLpNorm_count_lt_top, count_apply_finite', essInf_count_eq_ciInf, count_apply_eq_top', count_apply_lt_top', count_apply_finite, instIsNegInvariantCount, MeasureTheory.enorm_le_eLpNorm_count, MeasureTheory.integral_count, instIsMulRightInvariantCount, MeasureTheory.integrable_count_iff, ZMod.dft_eq_fourier, count_injective_image, MeasureTheory.count_real_singleton, MeasureTheory.hasFiniteIntegral_count_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_count_iff 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass count	—	instOuterMeasureClass Set.mem_empty_iff_false count_eq_zero_iff MeasureTheory.ae_iff MeasureTheory.ae_of_all
count_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count ENat.toENNReal Set.encard	—	sum_apply dirac_apply' ENNReal.tsum_one
count_apply_eq_top 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Top.top instTopENNReal Set.Infinite	—	count_apply_eq_top' Set.Finite.measurableSet count_apply_infinite
count_apply_eq_top' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Top.top instTopENNReal Set.Infinite	—	count_apply_finite' count_apply_infinite
count_apply_finite 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Set.Finite.toFinset	—	count_apply_finset Set.Finite.coe_toFinset
count_apply_finite' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Set.Finite.toFinset	—	count_apply_finset' Set.Finite.coe_toFinset
count_apply_finset 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count SetLike.coe Finset Finset.instSetLike AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card	—	count_apply_finset' Finset.measurableSet
count_apply_finset' 📖	mathematical	MeasurableSet SetLike.coe Finset Finset.instSetLike	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count SetLike.coe Finset Finset.instSetLike AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card	—	count_apply Set.encard_coe_eq_coe_finsetCard
count_apply_infinite 📖	mathematical	Set.Infinite	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Top.top instTopENNReal	—	top_unique le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat ENNReal.tendsto_nat_nhds_top Set.Infinite.exists_subset_card_eq Finset.sum_const nsmul_eq_mul mul_one Finset.tsum_subtype le_count_apply MeasureTheory.measure_mono instOuterMeasureClass
count_apply_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike count Top.top instTopENNReal Set.Finite	—	lt_top_iff_ne_top count_apply_eq_top
count_apply_lt_top' 📖	mathematical	MeasurableSet	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike count Top.top instTopENNReal Set.Finite	—	lt_top_iff_ne_top count_apply_eq_top'
count_eq_zero_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count instZeroENNReal Set.instEmptyCollection	—	Set.eq_empty_of_forall_notMem dirac_apply_of_mem ENNReal.instCanonicallyOrderedAdd NeZero.charZero_one ENNReal.instCharZero LE.le.trans_eq LE.le.trans ENNReal.le_tsum le_sum_apply MeasureTheory.measure_empty instOuterMeasureClass
count_injective_image 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Set.image	—	count_injective_image' Set.Finite.measurableSet Set.Finite.image count_apply_infinite Set.finite_image_iff Function.Injective.injOn
count_injective_image' 📖	mathematical	MeasurableSet Set.image	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Set.image	—	CanLift.prf Set.instCanLiftFinsetCoeFinite Finset.coe_image count_apply_finset' Finset.card_image_of_injective count_apply_infinite Set.finite_image_iff Function.Injective.injOn
count_ne_zero 📖	—	Set.Nonempty	—	—	count_ne_zero_iff
count_ne_zero'' 📖	—	—	—	—	—
count_ne_zero_iff 📖	mathematical	—	Set.Nonempty	—	Iff.not count_eq_zero_iff Set.nonempty_iff_ne_empty
count_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	count_singleton' MeasurableSingletonClass.measurableSet_singleton
count_singleton' 📖	mathematical	MeasurableSet Set Set.instSingletonSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Set.finite_singleton count_apply_finite' Set.Finite.toFinset.eq_1 Set.toFinset_singleton Finset.card_singleton Nat.cast_one
count_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike count Set.univ ENat.toENNReal ENat.card	—	count_apply MeasurableSet.univ Set.encard_univ
le_count_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal SummationFilter.unconditional DFunLike.coe MeasureTheory.Measure Set instFunLike count	—	tsum_subtype ENNReal.tsum_le_tsum le_dirac_apply le_sum_apply

MeasureTheory.Measure.count

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSigmaFinite 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Measure.count	—	MeasureTheory.Measure.count_singleton'
isFiniteMeasure 📖	mathematical	—	MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.count	—	MeasureTheory.Measure.count_apply Set.encard_univ

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_eq_dirac 📖	mathematical	—	MeasureTheory.Measure.count MeasureTheory.Measure.dirac	—	MeasureTheory.Measure.restrict_univ Set.ext IsScalarTower.right MeasureTheory.Measure.restrict_singleton MeasureTheory.Measure.count_singleton' measurableSingletonClass one_smul

Unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_eq_dirac 📖	mathematical	—	MeasureTheory.Measure.count MeasureTheory.Measure.dirac instInhabited	—	Subsingleton.count_eq_dirac instSubsingleton

---

← Back to Index