Countable

📁 Source: Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Statistics

Metric	Count
Definitions Countable	1
Theorems count_const_le_le_of_tsum_le, lintegral_lt_top_of_bounded_to_ennreal, exists_lt_lintegral_simpleFunc_of_lt_lintegral, exists_lt_lintegral_simpleFunc_of_lt_lintegral, exists_measurable_le_forall_setLIntegral_eq, exists_pos_lintegral_lt_of_sigmaFinite, iInf_le_lintegral, lintegral_const_lt_top, lintegral_count, lintegral_count', lintegral_countable, lintegral_countable', lintegral_dirac, lintegral_dirac', lintegral_eq_const, lintegral_finset, lintegral_fintype, lintegral_insert, lintegral_le_const, lintegral_le_iSup, lintegral_le_of_forall_fin_meas_le, lintegral_le_of_forall_fin_meas_le_of_measurable, lintegral_le_of_forall_fin_meas_trim_le, lintegral_singleton, lintegral_singleton', lintegral_unique, setLIntegral_const_lt_top, setLIntegral_dirac, setLIntegral_dirac', univ_le_of_forall_fin_meas_le, count_const_le_le_of_tsum_le	31
Total	32

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_const_le_le_of_tsum_le 📖	mathematical	Measurable ENNReal measurableSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum instAddCommMonoid instTopologicalSpace SummationFilter.unconditional	DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.count setOf DivInvMonoid.toDiv instDivInvMonoid	—	LE.le.trans MeasureTheory.meas_ge_le_lintegral_div Measurable.aemeasurable div_le_div MeasureTheory.lintegral_count Eq.le

IsFiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_lt_top_of_bounded_to_ennreal 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofNNReal	Preorder.toLT MeasureTheory.lintegral Top.top instTopENNReal	—	MeasureTheory.Measure.restrict_univ MeasureTheory.setLIntegral_lt_top_of_le_nnreal MeasureTheory.measure_ne_top

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_lintegral_simpleFunc_of_lt_lintegral 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder lintegral ENNReal.ofNNReal	NNReal Preorder.toLE instPartialOrderNNReal DFunLike.coe SimpleFunc SimpleFunc.instFunLike Top.top instTopENNReal	—	lintegral_eq_nnreal SimpleFunc.lintegral_eq_lintegral SimpleFunc.coe_map SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral LE.le.trans ENNReal.coe_le_coe
exists_measurable_le_forall_setLIntegral_eq 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	exists_measurable_le_lintegral_eq Measurable.iSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology instCountableNat iSup_le lintegral_eq_nnreal iSup₂_le Finset.bddAbove LE.le.trans SimpleFunc.mem_range_self Nat.le_ceil SimpleFunc.lintegral_eq_lintegral lintegral_mono le_min ENNReal.coe_le_coe LT.lt.ne IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal isFiniteMeasureRestrict min_le_right measurableSet_toMeasurable ENNReal.le_of_add_le_add_right Measure.restrict_toMeasurable_of_sFinite lintegral_add_compl add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid lintegral_mono_fn' le_refl le_iSup sum_sfiniteSeq Measure.restrict_sum_of_countable lintegral_sum_measure ENNReal.tsum_le_tsum instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite isFiniteMeasure_sfiniteSeq LE.le.antisymm
exists_pos_lintegral_lt_of_sigmaFinite 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Measurable NNReal.measurableSpace ENNReal ENNReal.instPartialOrder lintegral ENNReal.ofNNReal	—	LE.le.trans_lt measure_mono Measure.instOuterMeasureClass disjointed_subset measure_spanningSets_lt_top ENNReal.exists_pos_tsum_mul_lt_of_countable instCountableNat LT.lt.ne measurableSet_spanningSetsIndex preimage_spanningSetsIndex_singleton Measurable.comp measurable_from_nat lintegral_comp Measurable.coe_nnreal_ennreal lintegral_countable' Nat.instMeasurableSingletonClass Measure.map_apply mul_comm
iInf_le_lintegral 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder lintegral	—	le_trans IsProbabilityMeasure.measure_univ mul_one iInf_mul_le_lintegral
lintegral_const_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Top.top instTopENNReal	—	Measure.restrict_univ setLIntegral_const_lt_top
lintegral_count 📖	mathematical	—	lintegral Measure.count tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	Measure.count.eq_1 lintegral_sum_measure lintegral_dirac
lintegral_count' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.count tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	Measure.count.eq_1 lintegral_sum_measure lintegral_dirac'
lintegral_countable 📖	mathematical	—	lintegral Measure.restrict tsum ENNReal Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set Set.instMembership DFunLike.coe Measure Measure.instFunLike Set.instSingletonSet SummationFilter.unconditional	—	Set.biUnion_of_singleton lintegral_biUnion MeasurableSingletonClass.measurableSet_singleton Set.pairwiseDisjoint_fiber lintegral_singleton
lintegral_countable' 📖	mathematical	—	lintegral tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instSingletonSet SummationFilter.unconditional	—	IsScalarTower.right Measure.sum_smul_dirac lintegral_sum_measure lintegral_smul_measure lintegral_dirac mul_comm
lintegral_dirac 📖	mathematical	—	lintegral Measure.dirac	—	lintegral_congr_ae ae_eq_dirac lintegral_const IsProbabilityMeasure.measure_univ Measure.dirac.isProbabilityMeasure mul_one
lintegral_dirac' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.dirac	—	lintegral_congr_ae ae_eq_dirac' instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space lintegral_const IsProbabilityMeasure.measure_univ Measure.dirac.isProbabilityMeasure mul_one
lintegral_eq_const 📖	mathematical	Filter.Eventually ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral	—	Measure.instOuterMeasureClass lintegral_congr_ae lintegral_const IsProbabilityMeasure.measure_univ mul_one
lintegral_finset 📖	mathematical	—	lintegral Measure.restrict SetLike.coe Finset Finset.instSetLike Finset.sum ENNReal ENNReal.instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instSingletonSet	—	lintegral_countable Finset.countable_toSet
lintegral_fintype 📖	mathematical	—	lintegral Finset.sum ENNReal ENNReal.instAddCommMonoid Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instSingletonSet	—	lintegral_finset Finset.coe_univ Measure.restrict_univ
lintegral_insert 📖	mathematical	Set Set.instMembership	lintegral Measure.restrict Set.instInsert ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DFunLike.coe Measure Measure.instFunLike Set.instSingletonSet	—	Set.union_singleton lintegral_union MeasurableSingletonClass.measurableSet_singleton Set.disjoint_singleton_right lintegral_singleton add_comm
lintegral_le_const 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral	—	Measure.instOuterMeasureClass LE.le.trans_eq lintegral_mono_ae lintegral_const IsProbabilityMeasure.measure_univ mul_one
lintegral_le_iSup 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	le_trans lintegral_le_iSup_mul IsProbabilityMeasure.measure_univ mul_one
lintegral_le_of_forall_fin_meas_le 📖	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	—	le_rfl trim_eq_self lintegral_le_of_forall_fin_meas_trim_le
lintegral_le_of_forall_fin_meas_le_of_measurable 📖	—	MeasurableSpace MeasurableSpace.instLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	—	lintegral_le_of_forall_fin_meas_trim_le
lintegral_le_of_forall_fin_meas_trim_le 📖	—	MeasurableSpace MeasurableSpace.instLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	—	Measure.restrict_univ univ_le_of_forall_fin_meas_le setLIntegral_iUnion_of_directed instCountableNat directed_of_isDirected_le instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat le_refl
lintegral_singleton 📖	mathematical	—	lintegral Measure.restrict Set Set.instSingletonSet ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Measure.instFunLike	—	IsScalarTower.right Measure.restrict_singleton lintegral_smul_measure lintegral_dirac mul_comm
lintegral_singleton' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.restrict Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Measure.instFunLike	—	IsScalarTower.right Measure.restrict_singleton lintegral_smul_measure lintegral_dirac' mul_comm
lintegral_unique 📖	mathematical	—	lintegral ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Unique.instInhabited DFunLike.coe Measure Set Measure.instFunLike Set.univ	—	lintegral_congr Unique.forall_iff lintegral_const
setLIntegral_const_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict Top.top instTopENNReal	—	lintegral_const ENNReal.mul_lt_top Ne.lt_top measure_lt_top isFiniteMeasureRestrict
setLIntegral_dirac 📖	mathematical	—	lintegral Measure.restrict Measure.dirac ENNReal Set Set.instMembership instZeroENNReal	—	restrict_dirac lintegral_dirac lintegral_zero_measure
setLIntegral_dirac' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace MeasurableSet	lintegral Measure.restrict Measure.dirac Set Set.instMembership instZeroENNReal	—	restrict_dirac' lintegral_dirac' lintegral_zero_measure
univ_le_of_forall_fin_meas_le 📖	mathematical	MeasurableSpace MeasurableSpace.instLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	Set.univ	—	monotone_spanningSets measurableSet_spanningSets iUnion_spanningSets LE.le.trans iSup_le LT.lt.ne LE.le.trans_lt le_trim measure_spanningSets_lt_top

MeasureTheory.SimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_lintegral_simpleFunc_of_lt_lintegral 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral ENNReal.ofNNReal DFunLike.coe MeasureTheory.SimpleFunc NNReal instFunLike	Preorder.toLE instPartialOrderNNReal Top.top instTopENNReal	—	induction MulZeroClass.zero_mul ENNReal.not_lt_zero Set.piecewise_eq_indicator ENNReal.coe_indicator MeasureTheory.lintegral_indicator MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply' Set.univ_inter ENNReal.div_lt_iff mul_comm MeasureTheory.Measure.exists_subset_measure_lt_top Set.indicator_le_indicator_of_subset zero_le NNReal.instCanonicallyOrderedAdd ENNReal.mul_lt_top ENNReal.coe_lt_top MeasureTheory.lintegral_add_left Measurable.coe_nnreal_ennreal measurable zero_add LE.le.trans covariant_swap_add_of_covariant_add NNReal.addLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add NNReal.addLeftReflectLT add_zero IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd ENNReal.exists_lt_add_of_lt_add add_le_add lt_of_le_of_lt le_rfl ENNReal.add_lt_top LT.lt.trans LT.lt.trans_le ENNReal.add_lt_add

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_const_le_le_of_tsum_le 📖	mathematical	Measurable NNReal measurableSpace Summable NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum	ENNReal ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.count setOf DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofNNReal	—	ENNReal.count_const_le_le_of_tsum_le Measurable.comp measurable_coe_nnreal_ennreal ENNReal.tsum_coe_eq Summable.hasSum ENNReal.coe_le_coe Nat.cast_zero ENNReal.coe_ne_top

(root)

Definitions

Name	Category	Theorems
Countable 📖	CompData	107 math math: countable_iff_exists_injective, Function.Surjective.countable, Multiset.countable, instCountableFinsupp, Subgroup.instCountableSubtypeMulOppositeMemOp, Finsupp.instCountableSubtypeMemSubmoduleSpanRange, Function.Injective.countable, Set.Countable.of_preimage_singleton, instCountablePUnit, LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, Countable.of_equiv, CategoryTheory.CountableCategory.countableHom, instCountableInt, FirstOrder.Language.BoundedFormula.instCountableFormula, not_countable, instCountablePLift, Countable.of_linearOrder_locallyFiniteOrder, countable_right_of_prod_of_nonempty, Subgroup.instCountableSubtypeMemZpowers, Cardinal.mk_le_aleph0_iff, not_uncountable_iff, instCountablePProd, CategoryTheory.CountableCategory.countableObj, FirstOrder.Language.BoundedFormula.instCountableSymbolsWithConstants, instCountable_of_discrete_submodule, Encodable.List.Vector.countable, Nat.Partrec.Code.instCountableSubtypePFunPartrec, Pairwise.countable_of_isOpen_disjoint, Subsingleton.to_countable, FirstOrder.Language.BoundedFormula.instCountableSigmaNat, FirstOrder.Language.Term.instCountableOfSigmaNatFunctions, LightProfinite.instCountableDiscreteQuotient, countable_of_linear_succ_pred_arch, instCountablePSum, FirstOrder.Language.Countable.countable_functions, Uncountable.not_countable, Nat.Partrec.Code.instCountableSubtypeForallComputable, instCountableProd, Bool.countable, Set.countable_coe_iff, instCountableFreeGroup, Quotient.countable, FirstOrder.Language.exists_countable_is_age_of_iff, instCountablePNat, instCountableULift, countable_left_of_prod_of_nonempty, Subtype.countable, Function.Embedding.countable, instCountableSum, countable_of_Lindelof_of_discrete, FirstOrder.Language.Structure.Fg.instCountable_embedding, uncountable_iff_not_countable, CategoryTheory.discreteCountable, CategoryTheory.CountableCategory.instCountableHomHomAsType, Option.instCountable, Nat.Primes.countable, Prop.countable', Set.countable_univ_iff, FirstOrder.Language.countable_self_fgequiv_of_countable, countable_iff_exists_surjective, IterateMulAct.instCountable, SetCoe.countable, FirstOrder.Language.Structure.FG.countable_embedding, Equiv.countable_iff, CategoryTheory.CountableCategory.instCountableHomObjAsType, instCountableFreeAddMonoid, FirstOrder.Language.Substructure.instCountable_fg_substructures_of_countable, Array.countable, CategoryTheory.CountableCategory.instCountableHomAsType, instCountableQuotient, nonempty_denumerable_iff, AddSubgroup.instCountableSubtypeMemZMultiples, MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated, FirstOrder.Language.BoundedFormula.instCountableSymbolsConstantsOn, TopologicalSpace.Clopens.countable_prod, ProbabilityTheory.Kernel.condKernel_def, TopologicalSpace.Clopens.countable_iff_secondCountable, Set.Countable.to_subtype, Finite.to_countable, ENat.instCountable, Prop.countable, Encodable.nonempty_encodable, Finset.countable, IterateAddAct.instCountable, Set.Countable.substructure_closure, CategoryTheory.CountableCategory.instCountableObjAsType, not_countable_iff, countable_prod_swap, FirstOrder.Language.Structure.FG.countable_hom, countable_iff_nonempty_embedding, instCountableFreeAddGroup, FirstOrder.Language.Substructure.cg_iff_countable, TopologicalSpace.separableSpace_iff_countable, Encodable.countable, WithBot.instCountable, instCountableNat, instCountableFreeCommRing, FirstOrder.Language.Structure.cg_iff_countable, instCountableFreeAbelianGroup, List.countable, instCountableFreeMonoid, instCountableFin, WithTop.instCountable, FirstOrder.Language.Structure.FG.instCountable_hom, instCountableFreeRing, FirstOrder.Language.Substructure.countable_fg_substructures_of_countable, AddSubgroup.instCountableSubtypeAddOppositeMemOp

---

← Back to Index