Commit 2025-04-04 03:53 d635d41e

View on Github →

chore: split MeasureTheory.Measure.Typeclasses (#23649) The file has become a folder with four files in it:

.Finite for IsFiniteMeasure and IsLocallyFiniteMeasure
.SFinite for SFinite and SigmaFinite
.Probability for IsZeroOrProbabilityMeasure and IsProbabilityMeasure
.NoAtoms for NoAtoms

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Dynamics/Ergodic/Ergodic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Constructions/Projective.lean

Modified Mathlib/MeasureTheory/Decomposition/Exhaustion.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Sub.lean

Modified Mathlib/MeasureTheory/Measure/Trim.lean

Deleted Mathlib/MeasureTheory/Measure/Typeclasses.lean

deleted theorem Bornology.IsBounded.measure_lt_top

deleted theorem Finset.measure_zero

deleted theorem IsCompact.exists_open_superset_measure_lt_top'

deleted theorem IsCompact.exists_open_superset_measure_lt_top

deleted theorem IsCompact.measure_lt_top

deleted theorem IsCompact.measure_lt_top_of_nhdsWithin

deleted theorem IsCompact.measure_ne_top

deleted theorem IsCompact.measure_zero_of_nhdsWithin

deleted theorem MeasurableEmbedding.sigmaFinite_map

deleted theorem MeasurableEquiv.sigmaFinite_map

deleted theorem MeasureTheory.Ico_ae_eq_Icc

deleted theorem MeasureTheory.Ico_ae_eq_Ioc

deleted theorem MeasureTheory.Iio_ae_eq_Iic

deleted theorem MeasureTheory.Ioc_ae_eq_Icc

deleted theorem MeasureTheory.Ioi_ae_eq_Ici

deleted theorem MeasureTheory.Ioo_ae_eq_Icc

deleted theorem MeasureTheory.Ioo_ae_eq_Ico

deleted theorem MeasureTheory.Ioo_ae_eq_Ioc

deleted theorem MeasureTheory.IsProbabilityMeasure.ae_neBot

deleted theorem MeasureTheory.IsProbabilityMeasure.ne_zero

deleted theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis

deleted theorem MeasureTheory.Measure.FiniteAtFilter.filterSup

deleted theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono

deleted theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae

deleted theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff

deleted theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left

deleted theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right

deleted def MeasureTheory.Measure.FiniteAtFilter

deleted theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq

deleted def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE

deleted structure MeasureTheory.Measure.FiniteSpanningSetsIn

deleted theorem MeasureTheory.Measure.add_left_inj

deleted theorem MeasureTheory.Measure.add_right_inj

deleted theorem MeasureTheory.Measure.countable_meas_level_set_pos

deleted theorem MeasureTheory.Measure.countable_meas_level_set_pos₀

deleted theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion

deleted theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀

deleted theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top

deleted theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀

deleted theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn

deleted theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top

deleted theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos

deleted theorem MeasureTheory.Measure.exists_subset_measure_lt_top

deleted theorem MeasureTheory.Measure.finiteAtBot

deleted theorem MeasureTheory.Measure.finiteAtFilter_of_finite

deleted theorem MeasureTheory.Measure.finiteAt_nhds

deleted theorem MeasureTheory.Measure.finiteAt_nhdsWithin

deleted theorem MeasureTheory.Measure.finiteAt_principal

deleted def MeasureTheory.Measure.finiteSpanningSetsInCompact

deleted def MeasureTheory.Measure.finiteSpanningSetsInOpen

deleted theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion

deleted theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀

deleted theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero

deleted theorem MeasureTheory.Measure.iSup_restrict_spanningSets

deleted theorem MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet

deleted theorem MeasureTheory.Measure.isFiniteMeasure_map

deleted theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le

deleted theorem MeasureTheory.Measure.le_of_add_le_add_left

deleted theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover

deleted theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite

deleted theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum

deleted theorem MeasureTheory.Measure.restrict_singleton'

deleted theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover

deleted theorem MeasureTheory.Measure.restrict_toMeasurable_of_sFinite

deleted theorem MeasureTheory.Measure.sigmaFinite_of_countable

deleted theorem MeasureTheory.Measure.sigmaFinite_of_le

deleted theorem MeasureTheory.Measure.smul_finite

deleted def MeasureTheory.Measure.toFiniteSpanningSetsIn

deleted theorem MeasureTheory.SigmaFinite.of_map

deleted theorem MeasureTheory.SigmaFinite.out

deleted theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff'

deleted theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff

deleted theorem MeasureTheory.ae_eq_univ_iff_measure_eq

deleted theorem MeasureTheory.ae_iff_measure_eq

deleted theorem MeasureTheory.ae_iff_prob_eq_one

deleted theorem MeasureTheory.ae_mem_iff_measure_eq

deleted theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'

deleted theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict

deleted theorem MeasureTheory.coe_measureUnivNNReal

deleted theorem MeasureTheory.eq_zero_or_isProbabilityMeasure

deleted theorem MeasureTheory.eventually_mem_spanningSets

deleted theorem MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous

deleted theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage

deleted theorem MeasureTheory.exists_pos_ball

deleted theorem MeasureTheory.exists_pos_measure_of_cover

deleted theorem MeasureTheory.exists_pos_preimage_ball

deleted theorem MeasureTheory.ext_of_generate_finite

deleted theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite

deleted theorem MeasureTheory.iUnion_spanningSets

deleted theorem MeasureTheory.insert_ae_eq_self

deleted theorem MeasureTheory.inv_measure_univ_smul_eq_self

deleted theorem MeasureTheory.isCountablySpanning_spanningSets

deleted theorem MeasureTheory.isFiniteMeasure_of_le

deleted theorem MeasureTheory.isFiniteMeasure_restrict

deleted theorem MeasureTheory.isProbabilityMeasure_comap

deleted theorem MeasureTheory.isProbabilityMeasure_iff

deleted theorem MeasureTheory.isProbabilityMeasure_map

deleted theorem MeasureTheory.isZeroOrProbabilityMeasure_iff

deleted theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero

deleted theorem MeasureTheory.ite_ae_eq_of_measure_zero

deleted theorem MeasureTheory.measurableSet_spanningSets

deleted theorem MeasureTheory.measurableSet_spanningSetsIndex

deleted def MeasureTheory.measureUnivNNReal

deleted theorem MeasureTheory.measureUnivNNReal_eq_zero

deleted theorem MeasureTheory.measureUnivNNReal_pos

deleted theorem MeasureTheory.measureUnivNNReal_zero

deleted theorem MeasureTheory.measure_ball_lt_top

deleted theorem MeasureTheory.measure_closedBall_lt_top

deleted theorem MeasureTheory.measure_compl_le_add_iff

deleted theorem MeasureTheory.measure_compl_le_add_of_le_add

deleted theorem MeasureTheory.measure_lt_top

deleted theorem MeasureTheory.measure_ne_top

deleted theorem MeasureTheory.measure_spanningSets_lt_top

deleted theorem MeasureTheory.mem_ae_iff_prob_eq_one

deleted theorem MeasureTheory.mem_ae_iff_prob_eq_one₀

deleted theorem MeasureTheory.mem_disjointed_spanningSetsIndex

deleted theorem MeasureTheory.mem_spanningSetsIndex

deleted theorem MeasureTheory.mem_spanningSets_of_index_le

deleted theorem MeasureTheory.monotone_spanningSets

deleted theorem MeasureTheory.not_isFiniteMeasure_iff

deleted theorem MeasureTheory.one_le_prob_iff

deleted theorem MeasureTheory.preimage_spanningSetsIndex_singleton

deleted theorem MeasureTheory.prob_add_prob_compl

deleted theorem MeasureTheory.prob_compl_eq_one_iff

deleted theorem MeasureTheory.prob_compl_eq_one_iff₀

deleted theorem MeasureTheory.prob_compl_eq_one_sub

deleted theorem MeasureTheory.prob_compl_eq_one_sub₀

deleted theorem MeasureTheory.prob_compl_eq_zero_iff

deleted theorem MeasureTheory.prob_compl_eq_zero_iff₀

deleted theorem MeasureTheory.prob_compl_le_one_sub_of_le_prob

deleted theorem MeasureTheory.prob_compl_lt_one_sub_of_lt_prob

deleted theorem MeasureTheory.prob_le_one

deleted theorem MeasureTheory.restrict_Ico_eq_restrict_Icc

deleted theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc

deleted theorem MeasureTheory.restrict_Iio_eq_restrict_Iic

deleted theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc

deleted theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici

deleted theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc

deleted theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico

deleted theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc

deleted theorem MeasureTheory.restrict_compl_singleton

deleted theorem MeasureTheory.sfiniteSeq_le

deleted theorem MeasureTheory.sfiniteSeq_zero

deleted theorem MeasureTheory.sfinite_sum_of_countable

deleted theorem MeasureTheory.sigmaFinite_bot_iff

deleted theorem MeasureTheory.sigmaFinite_iff

deleted def MeasureTheory.spanningSets

deleted theorem MeasureTheory.spanningSetsIndex_eq_iff

deleted theorem MeasureTheory.spanningSets_mono

deleted theorem MeasureTheory.sum_restrict_disjointed_spanningSets

deleted theorem MeasureTheory.sum_sfiniteSeq

deleted theorem MeasureTheory.summable_measure_toReal

deleted theorem MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint

deleted theorem MeasureTheory.toReal_prob_le_one

deleted theorem MeasureTheory.uIoc_ae_eq_interval

deleted theorem Set.Countable.ae_not_mem

deleted theorem Set.Countable.measure_restrict_compl

deleted theorem Set.Countable.measure_zero

deleted theorem Set.Finite.measure_zero

deleted theorem Set.Infinite.meas_eq_top

deleted theorem Set.Subsingleton.measure_zero

deleted theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace

deleted theorem measure_Icc_lt_top

deleted theorem measure_Ico_lt_top

deleted theorem measure_Ioc_lt_top

deleted theorem measure_Ioo_lt_top

Created Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

added theorem Bornology.IsBounded.measure_lt_top

added theorem IsCompact.exists_open_superset_measure_lt_top'

added theorem IsCompact.exists_open_superset_measure_lt_top

added theorem IsCompact.measure_lt_top

added theorem IsCompact.measure_lt_top_of_nhdsWithin

added theorem IsCompact.measure_ne_top

added theorem IsCompact.measure_zero_of_nhdsWithin

added theorem MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis

added theorem MeasureTheory.Measure.FiniteAtFilter.filterSup

added theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono

added theorem MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae

added theorem MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff

added theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_left

added theorem MeasureTheory.Measure.FiniteAtFilter.inf_of_right

added def MeasureTheory.Measure.FiniteAtFilter

added structure MeasureTheory.Measure.FiniteSpanningSetsIn

added theorem MeasureTheory.Measure.exists_isOpen_measure_lt_top

added theorem MeasureTheory.Measure.finiteAtBot

added theorem MeasureTheory.Measure.finiteAtFilter_of_finite

added theorem MeasureTheory.Measure.finiteAt_nhds

added theorem MeasureTheory.Measure.finiteAt_nhdsWithin

added theorem MeasureTheory.Measure.finiteAt_principal

added def MeasureTheory.Measure.finiteSpanningSetsInCompact

added def MeasureTheory.Measure.finiteSpanningSetsInOpen

added theorem MeasureTheory.Measure.isFiniteMeasure_map

added theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_le

added theorem MeasureTheory.Measure.le_of_add_le_add_left

added theorem MeasureTheory.Measure.smul_finite

added theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff'

added theorem MeasureTheory.abs_toReal_measure_sub_le_measure_symmDiff

added theorem MeasureTheory.ae_eq_univ_iff_measure_eq

added theorem MeasureTheory.ae_iff_measure_eq

added theorem MeasureTheory.ae_mem_iff_measure_eq

added theorem MeasureTheory.coe_measureUnivNNReal

added theorem MeasureTheory.exists_ne_forall_mem_nhds_pos_measure_preimage

added theorem MeasureTheory.exists_pos_ball

added theorem MeasureTheory.exists_pos_measure_of_cover

added theorem MeasureTheory.exists_pos_preimage_ball

added theorem MeasureTheory.ext_of_generate_finite

added theorem MeasureTheory.ext_on_measurableSpace_of_generate_finite

added theorem MeasureTheory.isFiniteMeasure_of_le

added theorem MeasureTheory.isFiniteMeasure_restrict

added theorem MeasureTheory.ite_ae_eq_of_measure_compl_zero

added theorem MeasureTheory.ite_ae_eq_of_measure_zero

added def MeasureTheory.measureUnivNNReal

added theorem MeasureTheory.measureUnivNNReal_eq_zero

added theorem MeasureTheory.measureUnivNNReal_pos

added theorem MeasureTheory.measureUnivNNReal_zero

added theorem MeasureTheory.measure_ball_lt_top

added theorem MeasureTheory.measure_closedBall_lt_top

added theorem MeasureTheory.measure_compl_le_add_iff

added theorem MeasureTheory.measure_compl_le_add_of_le_add

added theorem MeasureTheory.measure_lt_top

added theorem MeasureTheory.measure_ne_top

added theorem MeasureTheory.not_isFiniteMeasure_iff

added theorem MeasureTheory.summable_measure_toReal

added theorem MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint

added theorem isFiniteMeasure_iff_isFiniteMeasureOnCompacts_of_compactSpace

added theorem measure_Icc_lt_top

added theorem measure_Ico_lt_top

added theorem measure_Ioc_lt_top

added theorem measure_Ioo_lt_top

Created Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

added theorem Finset.measure_zero

added theorem MeasureTheory.Ico_ae_eq_Icc

added theorem MeasureTheory.Ico_ae_eq_Ioc

added theorem MeasureTheory.Iio_ae_eq_Iic

added theorem MeasureTheory.Ioc_ae_eq_Icc

added theorem MeasureTheory.Ioi_ae_eq_Ici

added theorem MeasureTheory.Ioo_ae_eq_Icc

added theorem MeasureTheory.Ioo_ae_eq_Ico

added theorem MeasureTheory.Ioo_ae_eq_Ioc

added theorem MeasureTheory.Measure.restrict_singleton'

added theorem MeasureTheory.insert_ae_eq_self

added theorem MeasureTheory.restrict_Ico_eq_restrict_Icc

added theorem MeasureTheory.restrict_Ico_eq_restrict_Ioc

added theorem MeasureTheory.restrict_Iio_eq_restrict_Iic

added theorem MeasureTheory.restrict_Ioc_eq_restrict_Icc

added theorem MeasureTheory.restrict_Ioi_eq_restrict_Ici

added theorem MeasureTheory.restrict_Ioo_eq_restrict_Icc

added theorem MeasureTheory.restrict_Ioo_eq_restrict_Ico

added theorem MeasureTheory.restrict_Ioo_eq_restrict_Ioc

added theorem MeasureTheory.restrict_compl_singleton

added theorem MeasureTheory.uIoc_ae_eq_interval

added theorem Set.Countable.ae_not_mem

added theorem Set.Countable.measure_restrict_compl

added theorem Set.Countable.measure_zero

added theorem Set.Finite.measure_zero

added theorem Set.Subsingleton.measure_zero

Created Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

added theorem MeasureTheory.IsProbabilityMeasure.ae_neBot

added theorem MeasureTheory.IsProbabilityMeasure.ne_zero

added theorem MeasureTheory.ae_iff_prob_eq_one

added theorem MeasureTheory.eq_zero_or_isProbabilityMeasure

added theorem MeasureTheory.inv_measure_univ_smul_eq_self

added theorem MeasureTheory.isProbabilityMeasure_comap

added theorem MeasureTheory.isProbabilityMeasure_iff

added theorem MeasureTheory.isProbabilityMeasure_map

added theorem MeasureTheory.isZeroOrProbabilityMeasure_iff

added theorem MeasureTheory.mem_ae_iff_prob_eq_one

added theorem MeasureTheory.mem_ae_iff_prob_eq_one₀

added theorem MeasureTheory.one_le_prob_iff

added theorem MeasureTheory.prob_add_prob_compl

added theorem MeasureTheory.prob_compl_eq_one_iff

added theorem MeasureTheory.prob_compl_eq_one_iff₀

added theorem MeasureTheory.prob_compl_eq_one_sub

added theorem MeasureTheory.prob_compl_eq_one_sub₀

added theorem MeasureTheory.prob_compl_eq_zero_iff

added theorem MeasureTheory.prob_compl_eq_zero_iff₀

added theorem MeasureTheory.prob_compl_le_one_sub_of_le_prob

added theorem MeasureTheory.prob_compl_lt_one_sub_of_lt_prob

added theorem MeasureTheory.prob_le_one

added theorem MeasureTheory.toReal_prob_le_one

Created Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

added theorem MeasurableEmbedding.sigmaFinite_map

added theorem MeasurableEquiv.sigmaFinite_map

added theorem MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq

added def MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE

added theorem MeasureTheory.Measure.add_left_inj

added theorem MeasureTheory.Measure.add_right_inj

added theorem MeasureTheory.Measure.countable_meas_level_set_pos

added theorem MeasureTheory.Measure.countable_meas_level_set_pos₀

added theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion

added theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀

added theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top

added theorem MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀

added theorem MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn

added theorem MeasureTheory.Measure.exists_measure_inter_spanningSets_pos

added theorem MeasureTheory.Measure.exists_subset_measure_lt_top

added theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion

added theorem MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀

added theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero

added theorem MeasureTheory.Measure.iSup_restrict_spanningSets

added theorem MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet

added theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_cover

added theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite

added theorem MeasureTheory.Measure.measure_toMeasurable_inter_of_sum

added theorem MeasureTheory.Measure.restrict_toMeasurable_of_cover

added theorem MeasureTheory.Measure.restrict_toMeasurable_of_sFinite

added theorem MeasureTheory.Measure.sigmaFinite_of_countable

added theorem MeasureTheory.Measure.sigmaFinite_of_le

added def MeasureTheory.Measure.toFiniteSpanningSetsIn

added theorem MeasureTheory.SigmaFinite.of_map

added theorem MeasureTheory.SigmaFinite.out

added theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'

added theorem MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict

added theorem MeasureTheory.eventually_mem_spanningSets

added theorem MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous

added theorem MeasureTheory.iUnion_spanningSets

added theorem MeasureTheory.isCountablySpanning_spanningSets

added theorem MeasureTheory.measurableSet_spanningSets

added theorem MeasureTheory.measurableSet_spanningSetsIndex

added theorem MeasureTheory.measure_spanningSets_lt_top

added theorem MeasureTheory.mem_disjointed_spanningSetsIndex

added theorem MeasureTheory.mem_spanningSetsIndex

added theorem MeasureTheory.mem_spanningSets_of_index_le

added theorem MeasureTheory.monotone_spanningSets

added theorem MeasureTheory.preimage_spanningSetsIndex_singleton

added theorem MeasureTheory.sfiniteSeq_le

added theorem MeasureTheory.sfiniteSeq_zero

added theorem MeasureTheory.sfinite_sum_of_countable

added theorem MeasureTheory.sigmaFinite_bot_iff

added theorem MeasureTheory.sigmaFinite_iff

added def MeasureTheory.spanningSets

added theorem MeasureTheory.spanningSetsIndex_eq_iff

added theorem MeasureTheory.spanningSets_mono

added theorem MeasureTheory.sum_restrict_disjointed_spanningSets

added theorem MeasureTheory.sum_sfiniteSeq

added theorem Set.Infinite.meas_eq_top

Modified Mathlib/MeasureTheory/Topology.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified MathlibTest/finiteness.lean