Basic

📁 Source: Mathlib/MeasureTheory/VectorMeasure/Basic.lean

Statistics

Metric	Count
Definitions toENNRealVectorMeasure, toSignedMeasure, SignedMeasure, toMeasureOfLEZero, toMeasureOfZeroLE, toMeasureOfZeroLE', VectorMeasure, add, coeFnAddMonoidHom, dirac, ennrealToMeasure, equivMeasure, instAdd, instAddCommGroup, instAddCommMonoid, instCoeFun, instDistribMulAction, instInhabited, instModule, instNeg, instPartialOrder, instSMul, instSub, instZero, map, mapGm, mapRange, mapRangeHom, mapRangeₗ, mapₗ, measureOf', neg, restrict, restrictGm, restrictₗ, smul, sub, trim, «term_≤[_]_», «term_≪ᵥ_», «term_⟂ᵥ_»	41
Theorems toENNRealVectorMeasure_add, toENNRealVectorMeasure_apply, toENNRealVectorMeasure_apply_measurable, toENNRealVectorMeasure_ennrealToMeasure, toENNRealVectorMeasure_zero, toSignedMeasure_add, toSignedMeasure_apply, toSignedMeasure_apply_measurable, toSignedMeasure_congr, toSignedMeasure_eq_toSignedMeasure_iff, toSignedMeasure_le_toSignedMeasure_iff, toSignedMeasure_restrict_eq_restrict_toSignedMeasure, toSignedMeasure_smul, toSignedMeasure_sub_apply, toSignedMeasure_toMeasureOfZeroLE, toSignedMeasure_zero, zero_le_toSignedMeasure, toMeasureOfLEZero_apply, toMeasureOfLEZero_finite, toMeasureOfLEZero_real_apply, toMeasureOfLEZero_toSignedMeasure, toMeasureOfZeroLE_apply, toMeasureOfZeroLE_finite, toMeasureOfZeroLE_real_apply, toMeasureOfZeroLE_toSignedMeasure, add, ennrealToMeasure, eq, map, mk, neg_left, neg_right, refl, smul, sub, trans, zero, add_left, add_right, mk, neg_left, neg_left_iff, neg_right, neg_right_iff, smul_left, smul_right, zero_left, zero_right, add_apply, coeFnAddMonoidHom_apply, coe_add, coe_injective, coe_neg, coe_smul, coe_sub, coe_zero, dirac_apply_of_mem, dirac_apply_of_notMem, empty, empty', ennrealToMeasure_apply, ennrealToMeasure_toENNRealVectorMeasure, equivMeasure_apply, equivMeasure_symm_apply, exists_pos_measure_of_not_restrict_le_zero, ext, ext_iff, ext_iff', hasSum_of_disjoint_iUnion, instAddLeftMono, le_iff, le_iff', le_restrict_empty, le_restrict_univ_iff_le, m_iUnion, m_iUnion', mapGm_apply, mapRange_add, mapRange_apply, mapRange_id, mapRange_zero, map_add, map_apply, map_id, map_not_measurable, map_smul, map_zero, mapₗ_apply, measurable_of_not_restrict_le_zero, measurable_of_not_zero_le_restrict, neg_apply, neg_le_neg, neg_le_neg_iff, nonneg_of_zero_le_restrict, nonpos_of_restrict_le_zero, not_measurable, not_measurable', of_add_of_diff, of_biUnion_finset, of_compl, of_diff, of_diff_of_diff_eq_zero, of_disjoint_iUnion, of_iUnion_nonneg, of_iUnion_nonpos, of_nonneg_disjoint_union_eq_zero, of_nonpos_disjoint_union_eq_zero, of_union, restrictGm_apply, restrict_add, restrict_add_restrict_compl, restrict_apply, restrict_empty, restrict_eq_self, restrict_le_restrict_countable_iUnion, restrict_le_restrict_iUnion, restrict_le_restrict_iff, restrict_le_restrict_of_subset_le, restrict_le_restrict_subset, restrict_le_restrict_union, restrict_le_zero_of_not_measurable, restrict_le_zero_subset, restrict_neg, restrict_not_measurable, restrict_smul, restrict_sub, restrict_trim, restrict_univ, restrict_zero, restrictₗ_apply, smul_apply, sub_apply, subset_le_of_restrict_le_restrict, tendsto_vectorMeasure_iInter_atTop_nat, tendsto_vectorMeasure_iUnion_atTop_nat, trim_apply, trim_eq_self, trim_measurableSet_eq, zero_apply, zero_le_restrict_not_measurable, zero_le_restrict_subset, zero_trim	142
Total	183

MeasureTheory

Definitions

Name	Category	Theorems
SignedMeasure 📖	CompOp	49 math math: ComplexMeasure.equivSignedMeasure_symm_apply, Measure.toJordanDecomposition_toSignedMeasure_sub, Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure, Measure.toSignedMeasure_le_toSignedMeasure_iff, ComplexMeasure.HaveLebesgueDecomposition.imPart, Measure.sub_toSignedMeasure_eq_toSignedMeasure_sub, withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, SignedMeasure.toJordanDecomposition_zero, SignedMeasure.singularPart_smul, SignedMeasure.totalVariation_zero, SignedMeasure.toJordanDecomposition_smul_real, SignedMeasure.toMeasureOfLEZero_toSignedMeasure, ComplexMeasure.equivSignedMeasure_apply, SignedMeasure.singularPart_add, JordanDecomposition.toSignedMeasure_injective, SignedMeasure.re_toComplexMeasure, Measure.toSignedMeasure_smul, SignedMeasure.singularPart_zero, SignedMeasure.toJordanDecomposition_neg, SignedMeasure.singularPart_neg, SignedMeasure.haveLebesgueDecomposition_smul_real, Measure.toSignedMeasure_add, ComplexMeasure.HaveLebesgueDecomposition.rePart, SignedMeasure.rnDeriv_smul, SignedMeasure.haveLebesgueDecomposition_smul, SignedMeasure.totalVariation_neg, ComplexMeasure.im_apply, SignedMeasure.singularPart_sub, SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, SignedMeasure.singularPart_smul_nnreal, ComplexMeasure.equivSignedMeasureₗ_symm_apply, JordanDecomposition.toSignedMeasure_smul, JordanDecomposition.toSignedMeasure_neg, SignedMeasure.haveLebesgueDecomposition_neg, ComplexMeasure.absolutelyContinuous_ennreal_iff, SignedMeasure.rnDeriv_neg, Measure.toSignedMeasure_sub_apply, ComplexMeasure.re_apply, JordanDecomposition.toSignedMeasure_zero, ComplexMeasure.toComplexMeasure_to_signedMeasure, ComplexMeasure.equivSignedMeasureₗ_apply, SignedMeasure.toJordanDecompositionEquiv_apply, Measure.toSignedMeasure_zero, SignedMeasure.toJordanDecomposition_smul, Measure.zero_le_toSignedMeasure, SignedMeasure.im_toComplexMeasure, SignedMeasure.rnDeriv_add, SignedMeasure.rnDeriv_sub, SignedMeasure.toJordanDecompositionEquiv_symm_apply
VectorMeasure 📖	CompData	78 math math: VectorMeasure.restrict_empty, VectorMeasure.coeFnAddMonoidHom_apply, withDensityᵥ_sub, VectorMeasure.coe_smul, VectorMeasure.equivMeasure_apply, VectorMeasure.MutuallySingular.neg_right_iff, VectorMeasure.mapₗ_apply, SignedMeasure.exists_compl_positive_negative, VectorMeasure.restrict_le_restrict_of_subset_le, VectorMeasure.restrict_add, VectorMeasure.mapRange_add, VectorMeasure.smul_apply, VectorMeasure.neg_apply, VectorMeasure.MutuallySingular.neg_left_iff, VectorMeasure.coe_injective, withDensityᵥ_add', withDensityᵥ_neg', VectorMeasure.coe_neg, VectorMeasure.coe_zero, VectorMeasure.restrictₗ_apply, SignedMeasure.exists_isCompl_positive_negative, ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, VectorMeasure.MutuallySingular.zero_left, VectorMeasure.restrict_le_zero_of_not_measurable, VectorMeasure.mapRange_zero, VectorMeasure.MutuallySingular.zero_right, VectorMeasure.restrict_not_measurable, VectorMeasure.restrictGm_apply, VectorMeasure.coe_sub, VectorMeasure.zero_apply, VectorMeasure.AbsolutelyContinuous.neg_right, VectorMeasure.MutuallySingular.neg_right, VectorMeasure.AbsolutelyContinuous.add, VectorMeasure.neg_le_neg_iff, VectorMeasure.AbsolutelyContinuous.neg_left, VectorMeasure.AbsolutelyContinuous.sub, VectorMeasure.AbsolutelyContinuous.zero, VectorMeasure.map_smul, JordanDecomposition.exists_compl_positive_negative, VectorMeasure.MutuallySingular.smul_right, VectorMeasure.le_iff', Measure.toSignedMeasure_toMeasureOfZeroLE, VectorMeasure.equivMeasure_symm_apply, VectorMeasure.le_iff, VectorMeasure.le_restrict_empty, withDensityᵥ_neg, Measure.toENNRealVectorMeasure_add, VectorMeasure.map_add, VectorMeasure.zero_le_restrict_not_measurable, VectorMeasure.MutuallySingular.neg_left, VectorMeasure.zero_trim, VectorMeasure.coe_add, VectorMeasure.instAddLeftMono, VectorMeasure.restrict_smul, VectorMeasure.mapGm_apply, withDensityᵥ_add, SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, SignedMeasure.exists_subset_restrict_nonpos, withDensityᵥ_zero, VectorMeasure.MutuallySingular.smul_left, withDensityᵥ_sub', VectorMeasure.MutuallySingular.add_left, withDensityᵥ_smul, withDensityᵥ_smul', VectorMeasure.restrict_neg, VectorMeasure.restrict_add_restrict_compl, VectorMeasure.add_apply, VectorMeasure.map_zero, VectorMeasure.le_restrict_univ_iff_le, VectorMeasure.map_not_measurable, VectorMeasure.AbsolutelyContinuous.smul, VectorMeasure.MutuallySingular.add_right, Measure.toENNRealVectorMeasure_zero, Measure.toSignedMeasure_restrict_sub, VectorMeasure.restrict_zero, VectorMeasure.restrict_le_restrict_iff, VectorMeasure.sub_apply, VectorMeasure.restrict_sub
«term_≤[_]_» 📖	CompOp	—
«term_≪ᵥ_» 📖	CompOp	—
«term_⟂ᵥ_» 📖	CompOp	—

MeasureTheory.Measure

Definitions

Name	Category	Theorems
toENNRealVectorMeasure 📖	CompOp	11 math math: MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure, toENNRealVectorMeasure_apply, MeasureTheory.SignedMeasure.mutuallySingular_singularPart, MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, withDensityᵥ_absolutelyContinuous, MeasureTheory.VectorMeasure.equivMeasure_symm_apply, toENNRealVectorMeasure_add, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, toENNRealVectorMeasure_ennrealToMeasure, toENNRealVectorMeasure_apply_measurable, toENNRealVectorMeasure_zero
toSignedMeasure 📖	CompOp	20 math math: toJordanDecomposition_toSignedMeasure_sub, jordanDecompositionOfToSignedMeasureSub_toSignedMeasure, toSignedMeasure_le_toSignedMeasure_iff, sub_toSignedMeasure_eq_toSignedMeasure_sub, MeasureTheory.SignedMeasure.toMeasureOfZeroLE_toSignedMeasure, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure, toSignedMeasure_toMeasureOfZeroLE, toSignedMeasure_smul, toSignedMeasure_apply, toSignedMeasure_add, toSignedMeasure_congr, MeasureTheory.withDensityᵥ_toReal, toSignedMeasure_apply_measurable, toSignedMeasure_sub_apply, toSignedMeasure_restrict_eq_restrict_toSignedMeasure, toSignedMeasure_eq_toSignedMeasure_iff, toSignedMeasure_zero, toSignedMeasure_restrict_sub, zero_le_toSignedMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toENNRealVectorMeasure_add 📖	mathematical	—	toENNRealVectorMeasure MeasureTheory.Measure instAdd MeasureTheory.VectorMeasure ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.VectorMeasure.instAdd ENNReal.instContinuousAdd	—	MeasureTheory.VectorMeasure.ext ENNReal.instContinuousAdd toENNRealVectorMeasure_apply_measurable add_apply MeasureTheory.VectorMeasure.add_apply
toENNRealVectorMeasure_apply 📖	mathematical	—	MeasureTheory.VectorMeasure.measureOf' ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace toENNRealVectorMeasure MeasurableSet DFunLike.coe MeasureTheory.Measure Set instFunLike instZeroENNReal	—	—
toENNRealVectorMeasure_apply_measurable 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure.measureOf' ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace toENNRealVectorMeasure DFunLike.coe MeasureTheory.Measure Set instFunLike	—	—
toENNRealVectorMeasure_ennrealToMeasure 📖	mathematical	—	toENNRealVectorMeasure MeasureTheory.VectorMeasure.ennrealToMeasure	—	MeasureTheory.VectorMeasure.ext toENNRealVectorMeasure_apply_measurable MeasureTheory.VectorMeasure.ennrealToMeasure_apply
toENNRealVectorMeasure_zero 📖	mathematical	—	toENNRealVectorMeasure MeasureTheory.Measure instZero MeasureTheory.VectorMeasure ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.VectorMeasure.instZero	—	MeasureTheory.VectorMeasure.ext
toSignedMeasure_add 📖	mathematical	—	toSignedMeasure MeasureTheory.Measure instAdd MeasureTheory.isFiniteMeasureAdd MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instAdd Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	—	MeasureTheory.VectorMeasure.ext MeasureTheory.isFiniteMeasureAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toSignedMeasure_apply_measurable MeasureTheory.measureReal_add_apply MeasureTheory.measure_ne_top MeasureTheory.VectorMeasure.add_apply
toSignedMeasure_apply 📖	mathematical	—	MeasureTheory.VectorMeasure.measureOf' Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toSignedMeasure MeasurableSet real Real.instZero	—	—
toSignedMeasure_apply_measurable 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure.measureOf' Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toSignedMeasure real	—	—
toSignedMeasure_congr 📖	mathematical	—	toSignedMeasure	—	—
toSignedMeasure_eq_toSignedMeasure_iff 📖	mathematical	—	toSignedMeasure	—	ext MeasureTheory.measureReal_eq_measureReal_iff MeasureTheory.measure_ne_top toSignedMeasure_apply_measurable
toSignedMeasure_le_toSignedMeasure_iff 📖	mathematical	—	MeasureTheory.SignedMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Real.partialOrder toSignedMeasure MeasureTheory.Measure instPartialOrder	—	le_iff MeasureTheory.VectorMeasure.le_iff toSignedMeasure_apply_measurable real_def ENNReal.toReal_le_toReal MeasureTheory.measure_ne_top
toSignedMeasure_restrict_eq_restrict_toSignedMeasure 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure.restrict Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toSignedMeasure restrict MeasureTheory.isFiniteMeasureRestrict	—	MeasureTheory.VectorMeasure.ext MeasureTheory.isFiniteMeasureRestrict MeasureTheory.VectorMeasure.restrict_apply MeasureTheory.measureReal_restrict_apply
toSignedMeasure_smul 📖	mathematical	—	toSignedMeasure NNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right MeasureTheory.isFiniteMeasureSMulNNReal MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSMul Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSemiringNNReal NNReal.instDistribMulActionOfReal AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring Semiring.toModule SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.to_smulCommClass NNReal.instAlgebraOfReal Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instIsTopologicalRingReal	—	MeasureTheory.VectorMeasure.ext IsScalarTower.right MeasureTheory.isFiniteMeasureSMulNNReal SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toSignedMeasure_apply_measurable MeasureTheory.VectorMeasure.smul_apply MeasureTheory.measureReal_nnreal_smul_apply
toSignedMeasure_sub_apply 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure.measureOf' Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instSub Real.instAddCommGroup instIsTopologicalAddGroupReal toSignedMeasure Real.instSub real	—	instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.sub_apply toSignedMeasure_apply_measurable
toSignedMeasure_toMeasureOfZeroLE 📖	mathematical	—	MeasureTheory.SignedMeasure.toMeasureOfZeroLE toSignedMeasure Set.univ MeasurableSet.univ MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasureTheory.VectorMeasure.le_restrict_univ_iff_le zero_le_toSignedMeasure	—	ext MeasurableSet.univ MeasureTheory.VectorMeasure.le_restrict_univ_iff_le zero_le_toSignedMeasure CanLift.prf ENNReal.canLift LT.lt.ne MeasureTheory.measure_lt_top MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply Set.univ_inter
toSignedMeasure_zero 📖	mathematical	—	toSignedMeasure MeasureTheory.Measure instZero MeasureTheory.isFiniteMeasureZero MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instZero Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	MeasureTheory.VectorMeasure.ext MeasureTheory.isFiniteMeasureZero
zero_le_toSignedMeasure 📖	mathematical	—	MeasureTheory.SignedMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid Real.partialOrder MeasureTheory.VectorMeasure.instZero toSignedMeasure	—	MeasureTheory.VectorMeasure.le_restrict_univ_iff_le MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le toSignedMeasure_apply_measurable

MeasureTheory.SignedMeasure

Definitions

Name	Category	Theorems
toMeasureOfLEZero 📖	CompOp	5 math math: toMeasureOfLEZero_toSignedMeasure, toMeasureOfLEZero_apply, toMeasureOfLEZero_finite, toMeasureOfLEZero_real_apply, toJordanDecomposition_spec
toMeasureOfZeroLE 📖	CompOp	6 math math: toMeasureOfZeroLE_apply, toMeasureOfZeroLE_toSignedMeasure, MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE, toMeasureOfZeroLE_real_apply, toJordanDecomposition_spec, toMeasureOfZeroLE_finite
toMeasureOfZeroLE' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasureOfLEZero_apply 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike toMeasureOfLEZero ENNReal.ofNNReal Real.instLE Real.instZero Real.instNeg MeasureTheory.VectorMeasure.measureOf' Set.instInter AddCommGroup.toAddCommMonoid Real.instAddCommGroup MeasureTheory.VectorMeasure.instNeg instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid MeasureTheory.VectorMeasure.instAddCommGroup NegZeroClass.toZero MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply	—	instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfZeroLE_apply
toMeasureOfLEZero_finite 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	MeasureTheory.IsFiniteMeasure toMeasureOfLEZero	—	instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfLEZero_apply MeasurableSet.univ ENNReal.coe_lt_top
toMeasureOfLEZero_real_apply 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	MeasureTheory.Measure.real toMeasureOfLEZero Real.instNeg MeasureTheory.VectorMeasure.measureOf' Set Set.instInter	—	instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply toMeasureOfLEZero_apply
toMeasureOfLEZero_toSignedMeasure 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict Set.univ MeasureTheory.VectorMeasure.instZero	MeasureTheory.Measure.toSignedMeasure toMeasureOfLEZero MeasurableSet.univ toMeasureOfLEZero_finite MeasureTheory.SignedMeasure MeasureTheory.VectorMeasure.instNeg Real.instAddCommGroup instIsTopologicalAddGroupReal	—	MeasureTheory.VectorMeasure.ext MeasurableSet.univ toMeasureOfLEZero_finite instIsTopologicalAddGroupReal MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasureTheory.VectorMeasure.neg_le_neg Real.instIsOrderedAddMonoid neg_zero MeasureTheory.VectorMeasure.neg_apply Set.univ_inter toMeasureOfLEZero_apply
toMeasureOfZeroLE_apply 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike toMeasureOfZeroLE ENNReal.ofNNReal Real.instLE Real.instZero MeasureTheory.VectorMeasure.measureOf' Set.instInter MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left	—	MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left MeasurableSet.empty MeasurableSet.iUnion instCountableNat MeasureTheory.Measure.ofMeasurable_apply MeasureTheory.VectorMeasure.restrict_apply Set.inter_comm
toMeasureOfZeroLE_finite 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	MeasureTheory.IsFiniteMeasure toMeasureOfZeroLE	—	MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left toMeasureOfZeroLE_apply MeasurableSet.univ ENNReal.coe_lt_top
toMeasureOfZeroLE_real_apply 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero MeasurableSet	MeasureTheory.Measure.real toMeasureOfZeroLE MeasureTheory.VectorMeasure.measureOf' Set Set.instInter	—	MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left toMeasureOfZeroLE_apply
toMeasureOfZeroLE_toSignedMeasure 📖	mathematical	MeasureTheory.VectorMeasure Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder MeasureTheory.VectorMeasure.instPartialOrder Real.partialOrder MeasureTheory.VectorMeasure.restrict MeasureTheory.VectorMeasure.instZero Set.univ	MeasureTheory.Measure.toSignedMeasure toMeasureOfZeroLE MeasurableSet.univ toMeasureOfZeroLE_finite	—	MeasureTheory.VectorMeasure.ext MeasurableSet.univ toMeasureOfZeroLE_finite MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict MeasureTheory.VectorMeasure.zero_le_restrict_subset Set.inter_subset_left Set.univ_inter toMeasureOfZeroLE_apply

MeasureTheory.VectorMeasure

Definitions

Name	Category	Theorems
add 📖	CompOp	—
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
dirac 📖	CompOp	2 math math: dirac_apply_of_notMem, dirac_apply_of_mem
ennrealToMeasure 📖	CompOp	6 math math: equivMeasure_apply, ennrealToMeasure_toENNRealVectorMeasure, MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff, MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff, ennrealToMeasure_apply, MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure
equivMeasure 📖	CompOp	2 math math: equivMeasure_apply, equivMeasure_symm_apply
instAdd 📖	CompOp	18 math math: restrict_add, mapRange_add, MeasureTheory.withDensityᵥ_add', MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, AbsolutelyContinuous.add, MeasureTheory.SignedMeasure.singularPart_add, MeasureTheory.Measure.toSignedMeasure_add, MeasureTheory.Measure.toENNRealVectorMeasure_add, map_add, coe_add, instAddLeftMono, MeasureTheory.withDensityᵥ_add, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, MutuallySingular.add_left, restrict_add_restrict_compl, add_apply, MutuallySingular.add_right, MeasureTheory.SignedMeasure.rnDeriv_add
instAddCommGroup 📖	CompOp	1 math math: MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply
instAddCommMonoid 📖	CompOp	16 math math: coeFnAddMonoidHom_apply, mapₗ_apply, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, restrictₗ_apply, restrictGm_apply, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, MeasureTheory.SignedMeasure.re_toComplexMeasure, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, mapGm_apply, MeasureTheory.ComplexMeasure.im_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, MeasureTheory.ComplexMeasure.re_apply, MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, MeasureTheory.SignedMeasure.im_toComplexMeasure
instCoeFun 📖	CompOp	—
instDistribMulAction 📖	CompOp	—
instInhabited 📖	CompOp	—
instModule 📖	CompOp	13 math math: mapₗ_apply, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.imPart, restrictₗ_apply, MeasureTheory.ComplexMeasure.equivSignedMeasure_apply, MeasureTheory.SignedMeasure.re_toComplexMeasure, MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.rePart, MeasureTheory.ComplexMeasure.im_apply, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_symm_apply, MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff, MeasureTheory.ComplexMeasure.re_apply, MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure, MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply, MeasureTheory.SignedMeasure.im_toComplexMeasure
instNeg 📖	CompOp	21 math math: MutuallySingular.neg_right_iff, neg_apply, MutuallySingular.neg_left_iff, MeasureTheory.withDensityᵥ_neg', coe_neg, AbsolutelyContinuous.neg_right, MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure, MutuallySingular.neg_right, neg_le_neg_iff, AbsolutelyContinuous.neg_left, MeasureTheory.SignedMeasure.toJordanDecomposition_neg, MeasureTheory.SignedMeasure.singularPart_neg, MeasureTheory.withDensityᵥ_neg, MutuallySingular.neg_left, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, MeasureTheory.SignedMeasure.totalVariation_neg, MeasureTheory.JordanDecomposition.toSignedMeasure_neg, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_neg, MeasureTheory.SignedMeasure.rnDeriv_neg, restrict_neg, neg_le_neg
instPartialOrder 📖	CompOp	17 math math: MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iff, MeasureTheory.SignedMeasure.exists_compl_positive_negative, restrict_le_restrict_of_subset_le, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, restrict_le_zero_of_not_measurable, neg_le_neg_iff, MeasureTheory.JordanDecomposition.exists_compl_positive_negative, le_iff', MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE, le_iff, le_restrict_empty, zero_le_restrict_not_measurable, instAddLeftMono, MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos, le_restrict_univ_iff_le, restrict_le_restrict_iff, MeasureTheory.Measure.zero_le_toSignedMeasure
instSMul 📖	CompOp	18 math math: coe_smul, smul_apply, MeasureTheory.SignedMeasure.singularPart_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, map_smul, MutuallySingular.smul_right, MeasureTheory.Measure.toSignedMeasure_smul, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real, restrict_smul, MeasureTheory.SignedMeasure.rnDeriv_smul, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, MeasureTheory.JordanDecomposition.toSignedMeasure_smul, MutuallySingular.smul_left, MeasureTheory.withDensityᵥ_smul, MeasureTheory.withDensityᵥ_smul', AbsolutelyContinuous.smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul
instSub 📖	CompOp	14 math math: MeasureTheory.withDensityᵥ_sub, MeasureTheory.Measure.toJordanDecomposition_toSignedMeasure_sub, MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure, MeasureTheory.Measure.sub_toSignedMeasure_eq_toSignedMeasure_sub, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, coe_sub, AbsolutelyContinuous.sub, MeasureTheory.SignedMeasure.singularPart_sub, MeasureTheory.withDensityᵥ_sub', MeasureTheory.Measure.toSignedMeasure_sub_apply, MeasureTheory.Measure.toSignedMeasure_restrict_sub, sub_apply, restrict_sub, MeasureTheory.SignedMeasure.rnDeriv_sub
instZero 📖	CompOp	27 math math: restrict_empty, MeasureTheory.SignedMeasure.exists_compl_positive_negative, MeasureTheory.SignedMeasure.toJordanDecomposition_zero, coe_zero, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, MutuallySingular.zero_left, restrict_le_zero_of_not_measurable, mapRange_zero, MutuallySingular.zero_right, restrict_not_measurable, MeasureTheory.SignedMeasure.totalVariation_zero, zero_apply, AbsolutelyContinuous.zero, MeasureTheory.JordanDecomposition.exists_compl_positive_negative, MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE, MeasureTheory.SignedMeasure.singularPart_zero, zero_le_restrict_not_measurable, zero_trim, MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos, MeasureTheory.withDensityᵥ_zero, MeasureTheory.JordanDecomposition.toSignedMeasure_zero, map_zero, map_not_measurable, MeasureTheory.Measure.toSignedMeasure_zero, MeasureTheory.Measure.toENNRealVectorMeasure_zero, restrict_zero, MeasureTheory.Measure.zero_le_toSignedMeasure
map 📖	CompOp	9 math math: mapₗ_apply, AbsolutelyContinuous.map, map_smul, map_add, mapGm_apply, map_apply, map_zero, map_not_measurable, map_id
mapGm 📖	CompOp	1 math math: mapGm_apply
mapRange 📖	CompOp	6 math math: mapRange_id, mapRange_add, mapRange_zero, mapRange_apply, MeasureTheory.ComplexMeasure.im_apply, MeasureTheory.ComplexMeasure.re_apply
mapRangeHom 📖	CompOp	—
mapRangeₗ 📖	CompOp	—
mapₗ 📖	CompOp	1 math math: mapₗ_apply
measureOf' 📖	CompOp	66 math math: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, coeFnAddMonoidHom_apply, restrict_eq_self, coe_smul, not_measurable', empty, trim_measurableSet_eq, MeasureTheory.SignedMeasure.toComplexMeasure_apply, smul_apply, neg_apply, MeasureTheory.Measure.toENNRealVectorMeasure_apply, coe_injective, coe_neg, coe_zero, hasSum_of_disjoint_iUnion, not_measurable, coe_sub, ext_iff', subset_le_of_restrict_le_restrict, zero_apply, mapRange_apply, restrict_apply, isSigmaSubadditiveSetFun_enorm, nonpos_of_restrict_le_zero, m_iUnion', ennrealToMeasure_apply, le_iff', of_union, MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply, AbsolutelyContinuous.ennrealToMeasure, le_iff, MeasureTheory.Measure.toSignedMeasure_apply, of_diff, exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom, empty', of_biUnion_finset, of_disjoint_iUnion, coe_add, MeasureTheory.SignedMeasure.toComplexMeasure_apply_re, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, MeasureTheory.withDensityᵥ_apply, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, nonneg_of_zero_le_restrict, dirac_apply_of_notMem, tendsto_vectorMeasure_iInter_atTop_nat, ext_iff, MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply, MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative, map_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable, exists_extension_of_isSetSemiring_of_le_measure_of_dense, MeasureTheory.Measure.toSignedMeasure_sub_apply, add_apply, MeasureTheory.SignedMeasure.toComplexMeasure_apply_im, MeasureTheory.SignedMeasure.null_of_totalVariation_zero, m_iUnion, MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable, exists_extension_of_isSetRing_of_le_measure_of_dense, tendsto_vectorMeasure_iUnion_atTop_nat, dirac_apply_of_mem, trim_apply, restrict_le_restrict_iff, sub_apply, of_compl, exists_pos_measure_of_not_restrict_le_zero, of_add_of_diff
neg 📖	CompOp	—
restrict 📖	CompOp	28 math math: restrict_empty, restrict_eq_self, MeasureTheory.SignedMeasure.exists_compl_positive_negative, restrict_le_restrict_of_subset_le, restrict_add, restrictₗ_apply, MeasureTheory.SignedMeasure.exists_isCompl_positive_negative, restrict_le_zero_of_not_measurable, restrict_not_measurable, restrictGm_apply, restrict_trim, restrict_apply, neg_le_neg_iff, MeasureTheory.JordanDecomposition.exists_compl_positive_negative, MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE, le_restrict_empty, zero_le_restrict_not_measurable, restrict_univ, restrict_smul, MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos, restrict_neg, restrict_add_restrict_compl, MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure, le_restrict_univ_iff_le, MeasureTheory.Measure.toSignedMeasure_restrict_sub, restrict_zero, restrict_le_restrict_iff, restrict_sub
restrictGm 📖	CompOp	1 math math: restrictGm_apply
restrictₗ 📖	CompOp	1 math math: restrictₗ_apply
smul 📖	CompOp	—
sub 📖	CompOp	—
trim 📖	CompOp	8 math math: trim_eq_self, trim_measurableSet_eq, restrict_trim, MeasureTheory.rnDeriv_ae_eq_condExp, zero_trim, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, trim_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom MeasureTheory.VectorMeasure AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addZeroClass Set AddMonoidHom.instFunLike coeFnAddMonoidHom measureOf'	—	—
coe_add 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instAdd Pi.instAdd Set AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_injective 📖	mathematical	—	MeasureTheory.VectorMeasure measureOf'	—	—
coe_neg 📖	mathematical	—	measureOf' AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instNeg Pi.instNeg Set NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_smul 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instSMul Function.hasSMul Set SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
coe_sub 📖	mathematical	—	measureOf' AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instSub Pi.instSub Set SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_zero 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instZero Pi.instZero Set AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
dirac_apply_of_mem 📖	mathematical	MeasurableSet Set Set.instMembership	measureOf' dirac	—	—
dirac_apply_of_notMem 📖	mathematical	Set Set.instMembership	measureOf' dirac AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
empty 📖	mathematical	—	measureOf' Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	empty'
empty' 📖	mathematical	—	measureOf' Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
ennrealToMeasure_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ennrealToMeasure measureOf' ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace	—	empty of_disjoint_iUnion instCountableNat ENNReal.instT2Space ennrealToMeasure.eq_1 MeasureTheory.Measure.ofMeasurable_apply
ennrealToMeasure_toENNRealVectorMeasure 📖	mathematical	—	ennrealToMeasure MeasureTheory.Measure.toENNRealVectorMeasure	—	MeasureTheory.Measure.ext ennrealToMeasure_apply MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
equivMeasure_apply 📖	mathematical	—	DFunLike.coe Equiv MeasureTheory.VectorMeasure ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace MeasureTheory.Measure EquivLike.toFunLike Equiv.instEquivLike equivMeasure ennrealToMeasure	—	—
equivMeasure_symm_apply 📖	mathematical	—	DFunLike.coe Equiv MeasureTheory.Measure MeasureTheory.VectorMeasure ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivMeasure MeasureTheory.Measure.toENNRealVectorMeasure	—	—
exists_pos_measure_of_not_restrict_le_zero 📖	mathematical	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder restrict instZero	MeasurableSet Set Set.instHasSubset Preorder.toLT AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid measureOf'	—	measurable_of_not_restrict_le_zero Mathlib.Tactic.Push.not_forall_eq restrict_le_restrict_iff
ext 📖	—	measureOf'	—	—	ext_iff
ext_iff 📖	mathematical	—	measureOf'	—	ext_iff' not_measurable
ext_iff' 📖	mathematical	—	measureOf'	—	coe_injective
hasSum_of_disjoint_iUnion 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	HasSum measureOf' Set.iUnion SummationFilter.unconditional	—	Countable.exists_injective_nat hasSum_extend_zero Function.apply_extend empty iSup_extend_bot m_iUnion Function.extend_const Pairwise.disjoint_extend_bot Function.Injective.factorsThrough
instAddLeftMono 📖	mathematical	—	AddLeftMono MeasureTheory.VectorMeasure instAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	le_imp_le_of_le_of_le add_le_add_right le_refl
le_iff 📖	mathematical	—	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder measureOf'	—	—
le_iff' 📖	mathematical	—	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder measureOf'	—	not_measurable le_refl
le_restrict_empty 📖	mathematical	—	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set Set.instEmptyCollection	—	restrict_empty
le_restrict_univ_iff_le 📖	mathematical	—	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set.univ	—	restrict_univ
m_iUnion 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	HasSum measureOf' Set.iUnion SummationFilter.unconditional	—	m_iUnion'
m_iUnion' 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	HasSum measureOf' Set.iUnion SummationFilter.unconditional	—	—
mapGm_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom MeasureTheory.VectorMeasure AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddMonoidHom.instFunLike mapGm map	—	—
mapRange_add 📖	mathematical	Continuous DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	mapRange MeasureTheory.VectorMeasure instAdd	—	ext map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
mapRange_apply 📖	mathematical	Continuous DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	measureOf' mapRange	—	—
mapRange_id 📖	mathematical	—	mapRange AddMonoidHom.id AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid continuous_id	—	ext continuous_id
mapRange_zero 📖	mathematical	Continuous DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	mapRange MeasureTheory.VectorMeasure instZero	—	ext map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
map_add 📖	mathematical	—	map MeasureTheory.VectorMeasure instAdd	—	ext map_apply add_zero
map_apply 📖	mathematical	Measurable MeasurableSet	measureOf' map Set.preimage	—	map.eq_1
map_id 📖	mathematical	—	map	—	ext map_apply measurable_id Set.preimage_id
map_not_measurable 📖	mathematical	Measurable	map MeasureTheory.VectorMeasure instZero	—	—
map_smul 📖	mathematical	—	map MeasureTheory.VectorMeasure instSMul	—	ext map_apply smul_zero
map_zero 📖	mathematical	—	map MeasureTheory.VectorMeasure instZero	—	ext map_apply zero_apply
mapₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MeasureTheory.VectorMeasure instAddCommMonoid instModule LinearMap.instFunLike mapₗ map	—	—
measurable_of_not_restrict_le_zero 📖	mathematical	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	MeasurableSet	—	Not.imp_symm restrict_le_zero_of_not_measurable
measurable_of_not_zero_le_restrict 📖	mathematical	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	MeasurableSet	—	Not.imp_symm zero_le_restrict_not_measurable
neg_apply 📖	mathematical	—	measureOf' AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
neg_le_neg 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	instNeg	—	restrict_apply neg_apply neg_le_neg
neg_le_neg_iff 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instNeg	—	neg_le_neg neg_neg
nonneg_of_zero_le_restrict 📖	mathematical	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid measureOf'	—	restrict_le_restrict_iff Set.Subset.rfl not_measurable le_refl
nonpos_of_restrict_le_zero 📖	mathematical	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	restrict_le_restrict_iff Set.Subset.rfl not_measurable le_refl
not_measurable 📖	mathematical	MeasurableSet	measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	not_measurable'
not_measurable' 📖	mathematical	MeasurableSet	measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
of_add_of_diff 📖	mathematical	MeasurableSet Set Set.instHasSubset	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup measureOf' Set.instSDiff	—	of_union Set.disjoint_sdiff_right MeasurableSet.diff Set.union_diff_cancel
of_biUnion_finset 📖	mathematical	Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset Finset.instSetLike MeasurableSet	measureOf' Set.iUnion Finset.instMembership Finset.sum	—	Finset.induction Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty empty Set.iUnion_iUnion_eq_or_left Finset.sum_insert of_union Finset.coe_insert Finset.measurableSet_biUnion Set.PairwiseDisjoint.subset
of_compl 📖	mathematical	MeasurableSet	measureOf' AddCommGroup.toAddCommMonoid Compl.compl Set Set.instCompl SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.univ	—	Set.compl_eq_univ_diff of_diff MeasurableSet.univ Set.subset_univ
of_diff 📖	mathematical	MeasurableSet Set Set.instHasSubset	measureOf' AddCommGroup.toAddCommMonoid Set.instSDiff SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	of_add_of_diff add_sub_cancel_left
of_diff_of_diff_eq_zero 📖	mathematical	MeasurableSet measureOf' Set Set.instSDiff AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.diff_union_inter of_union disjoint_comm Set.disjoint_of_subset_left Set.inter_subset_right disjoint_sdiff_self_right MeasurableSet.diff MeasurableSet.inter Set.inter_subset_left add_zero Set.union_comm Set.inter_comm
of_disjoint_iUnion 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	measureOf' Set.iUnion tsum SummationFilter.unconditional	—	HasSum.tsum_eq SummationFilter.instNeBotUnconditional hasSum_of_disjoint_iUnion
of_iUnion_nonneg 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid measureOf'	Set.iUnion	—	tsum_nonneg of_disjoint_iUnion OrderClosedTopology.to_t2Space
of_iUnion_nonpos 📖	mathematical	MeasurableSet Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Preorder.toLE PartialOrder.toPreorder measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Set.iUnion	—	tsum_nonpos of_disjoint_iUnion OrderClosedTopology.to_t2Space
of_nonneg_disjoint_union_eq_zero 📖	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet Real Real.instLE Real.instZero measureOf' Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.instUnion	—	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Linarith.le_of_le_of_eq sub_eq_zero_of_eq of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
of_nonpos_disjoint_union_eq_zero 📖	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet Real Real.instLE measureOf' Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.instUnion	—	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.le_of_le_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq of_union TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Mathlib.Tactic.Linarith.sub_neg_of_lt
of_union 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	measureOf' Set.instUnion AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.union_eq_iUnion of_disjoint_iUnion Bool.countable pairwise_disjoint_on_bool tsum_fintype SummationFilter.instLeAtTopUnconditional Fintype.sum_bool
restrictGm_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom MeasureTheory.VectorMeasure AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid AddMonoidHom.instFunLike restrictGm restrict	—	—
restrict_add 📖	mathematical	—	restrict MeasureTheory.VectorMeasure instAdd	—	ext restrict_apply restrict_not_measurable add_zero
restrict_add_restrict_compl 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure instAdd restrict Compl.compl Set Set.instCompl	—	ext add_apply restrict_apply MeasurableSet.compl of_union Disjoint.inter_left' Disjoint.inter_right' disjoint_compl_right MeasurableSet.inter Set.inter_union_compl
restrict_apply 📖	mathematical	MeasurableSet	measureOf' restrict Set Set.instInter	—	restrict.eq_1
restrict_empty 📖	mathematical	—	restrict Set Set.instEmptyCollection MeasureTheory.VectorMeasure instZero	—	ext restrict_apply MeasurableSet.empty Set.inter_empty empty zero_apply
restrict_eq_self 📖	mathematical	MeasurableSet Set Set.instHasSubset	measureOf' restrict	—	restrict_apply Set.inter_eq_left
restrict_le_restrict_countable_iUnion 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	Set.iUnion	—	nonempty_encodable Encodable.iUnion_decode₂ restrict_le_restrict_iUnion Set.iUnion_congr_Prop MeasurableSet.iUnion Prop.countable Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty restrict_empty Set.iUnion_iUnion_eq_right
restrict_le_restrict_iUnion 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	Set.iUnion	—	restrict_le_restrict_of_subset_le Set.inter_iUnion iUnion_disjointed Set.inter_eq_left Pairwise.mono disjoint_disjointed Disjoint.mono inf_le_right of_disjoint_iUnion instCountableNat OrderClosedTopology.to_t2Space MeasurableSet.inter MeasurableSet.disjointed Summable.tsum_le_tsum SummationFilter.instNeBotUnconditional restrict_le_restrict_iff Set.Subset.trans Set.inter_subset_right disjointed_subset HasSum.summable m_iUnion
restrict_le_restrict_iff 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict measureOf'	—	restrict_eq_self le_iff MeasurableSet.inter Set.inter_subset_right restrict_apply
restrict_le_restrict_of_subset_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder measureOf'	MeasureTheory.VectorMeasure instPartialOrder restrict	—	restrict_le_restrict_iff restrict_not_measurable le_refl
restrict_le_restrict_subset 📖	—	MeasurableSet MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set Set.instHasSubset	—	—	restrict_le_restrict_of_subset_le subset_le_of_restrict_le_restrict Set.Subset.trans
restrict_le_restrict_union 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict	Set Set.instUnion	—	Set.union_eq_iUnion restrict_le_restrict_countable_iUnion Bool.countable
restrict_le_zero_of_not_measurable 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	—	restrict_zero restrict_not_measurable le_refl
restrict_le_zero_subset 📖	—	MeasurableSet Set Set.instHasSubset MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	—	—	restrict_le_restrict_of_subset_le restrict_le_restrict_iff Set.Subset.trans
restrict_neg 📖	mathematical	—	restrict AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instNeg	—	ext restrict_apply restrict_not_measurable neg_zero
restrict_not_measurable 📖	mathematical	MeasurableSet	restrict MeasureTheory.VectorMeasure instZero	—	—
restrict_smul 📖	mathematical	—	restrict MeasureTheory.VectorMeasure instSMul	—	ext restrict_apply restrict_not_measurable smul_zero
restrict_sub 📖	mathematical	—	restrict AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instSub	—	sub_eq_add_neg restrict_add restrict_neg
restrict_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	restrict trim	—	ext restrict_apply trim_measurableSet_eq
restrict_univ 📖	mathematical	—	restrict Set.univ	—	ext restrict_apply MeasurableSet.univ Set.inter_univ
restrict_zero 📖	mathematical	—	restrict MeasureTheory.VectorMeasure instZero	—	ext restrict_apply zero_apply
restrictₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring MeasureTheory.VectorMeasure instAddCommMonoid instModule LinearMap.instFunLike restrictₗ restrict	—	—
smul_apply 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
sub_apply 📖	mathematical	—	measureOf' AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
subset_le_of_restrict_le_restrict 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict Set Set.instHasSubset	measureOf'	—	restrict_le_restrict_iff not_measurable le_refl
tendsto_vectorMeasure_iInter_atTop_nat 📖	mathematical	Antitone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MeasurableSet	Filter.Tendsto measureOf' AddCommGroup.toAddCommMonoid Filter.atTop nhds Set.iInter	—	of_compl sub_sub_cancel MeasurableSet.iUnion instCountableNat MeasurableSet.compl Set.compl_iUnion compl_compl Filter.Tendsto.sub tendsto_const_nhds tendsto_vectorMeasure_iUnion_atTop_nat
tendsto_vectorMeasure_iUnion_atTop_nat 📖	mathematical	Monotone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MeasurableSet	Filter.Tendsto measureOf' Filter.atTop nhds Set.iUnion	—	MeasurableSet.disjointed iUnion_disjointed m_iUnion disjoint_disjointed of_biUnion_finset biUnion_range_succ_disjointed Monotone.partialSups_eq Filter.Tendsto.comp HasSum.tendsto_sum_nat Filter.tendsto_add_atTop_nat
trim_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	measureOf' trim MeasurableSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
trim_eq_self 📖	mathematical	—	trim le_rfl MeasurableSpace PartialOrder.toPreorder MeasurableSpace.instPartialOrder	—	ext le_rfl
trim_measurableSet_eq 📖	mathematical	MeasurableSpace MeasurableSpace.instLE MeasurableSet	measureOf' trim	—	—
zero_apply 📖	mathematical	—	measureOf' MeasureTheory.VectorMeasure instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
zero_le_restrict_not_measurable 📖	mathematical	MeasurableSet	MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	—	restrict_zero restrict_not_measurable le_refl
zero_le_restrict_subset 📖	—	MeasurableSet Set Set.instHasSubset MeasureTheory.VectorMeasure Preorder.toLE PartialOrder.toPreorder instPartialOrder restrict instZero	—	—	restrict_le_restrict_of_subset_le restrict_le_restrict_iff Set.Subset.trans
zero_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE	trim MeasureTheory.VectorMeasure instZero	—	ext

MeasureTheory.VectorMeasure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instAdd	—	MeasureTheory.VectorMeasure.add_apply zero_add
ennrealToMeasure 📖	mathematical	—	MeasureTheory.VectorMeasure.measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MeasureTheory.VectorMeasure.AbsolutelyContinuous ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace	—	MeasureTheory.VectorMeasure.ennrealToMeasure_apply MeasureTheory.VectorMeasure.not_measurable
eq 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous	—	—
map 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous	MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.VectorMeasure.map	—	MeasureTheory.VectorMeasure.map_apply MeasureTheory.VectorMeasure.map_not_measurable MeasureTheory.VectorMeasure.zero_apply
mk 📖	mathematical	MeasureTheory.VectorMeasure.measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	MeasureTheory.VectorMeasure.AbsolutelyContinuous	—	MeasureTheory.VectorMeasure.not_measurable
neg_left 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous AddCommGroup.toAddCommMonoid	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	MeasureTheory.VectorMeasure.neg_apply neg_zero
neg_right 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous AddCommGroup.toAddCommMonoid	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	neg_eq_zero MeasureTheory.VectorMeasure.neg_apply
refl 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous	—	eq
smul 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instSMul	—	MeasureTheory.VectorMeasure.smul_apply smul_zero
sub 📖	mathematical	MeasureTheory.VectorMeasure.AbsolutelyContinuous AddCommGroup.toAddCommMonoid	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instSub	—	MeasureTheory.VectorMeasure.sub_apply zero_sub neg_zero
trans 📖	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous	—	—	—
zero 📖	mathematical	—	MeasureTheory.VectorMeasure.AbsolutelyContinuous MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instZero	—	MeasureTheory.VectorMeasure.zero_apply

MeasureTheory.VectorMeasure.MutuallySingular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_left 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instAdd	—	MeasurableSet.inter MeasureTheory.VectorMeasure.add_apply Set.subset_inter_iff zero_add Set.Subset.antisymm Set.compl_inter MeasureTheory.VectorMeasure.of_union Disjoint.mono Set.inter_subset_left disjoint_sdiff_self_right MeasurableSet.compl MeasurableSet.diff Set.Subset.trans Set.diff_subset add_zero
add_right 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instAdd	—	symm add_left
mk 📖	mathematical	MeasurableSet MeasureTheory.VectorMeasure.measureOf' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	MeasureTheory.VectorMeasure.MutuallySingular	—	MeasureTheory.VectorMeasure.not_measurable
neg_left 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular AddCommGroup.toAddCommMonoid	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	MeasureTheory.VectorMeasure.neg_apply neg_eq_zero
neg_left_iff 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	neg_left neg_neg
neg_right 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular AddCommGroup.toAddCommMonoid	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	symm neg_left
neg_right_iff 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular AddCommGroup.toAddCommMonoid MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instNeg	—	neg_right neg_neg
smul_left 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instSMul	—	symm smul_right
smul_right 📖	mathematical	MeasureTheory.VectorMeasure.MutuallySingular	MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instSMul	—	smul_zero
zero_left 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instZero	—	symm zero_right
zero_right 📖	mathematical	—	MeasureTheory.VectorMeasure.MutuallySingular MeasureTheory.VectorMeasure MeasureTheory.VectorMeasure.instZero	—	MeasurableSet.empty MeasureTheory.VectorMeasure.empty Set.subset_empty_iff MeasureTheory.VectorMeasure.zero_apply

---

← Back to Index