FiniteMeasure

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

Statistics

Metric	Count
Definitions `FiniteMeasure`, `comap`, `instAdd`, `instAddCommMonoid`, `instCoe`, `instFunLike`, `instInhabited`, `instMeasurableSpace`, `instModuleNNReal`, `instSMul`, `instTopologicalSpace`, `instZero`, `map`, `mapCLM`, `mapHom`, `mass`, `restrict`, `testAgainstNN`, `toMeasure`, `toMeasureAddMonoidHom`, `toWeakDualBCNN`	21
Theorems `mass`, `isEmbedding_map_finiteMeasure`, `apply_iUnion_le`, `apply_le_mass`, `apply_mono`, `apply_union_le`, `coeFn_add`, `coeFn_def`, `coeFn_mk`, `coeFn_smul`, `coeFn_zero`, `coe_toWeakDualBCNN`, `continuous_iff_forall_continuousMap_continuous_integral`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `continuous_iff_forall_continuous_integral`, `continuous_iff_forall_continuous_lintegral`, `continuous_integral_boundedContinuousFunction`, `continuous_integral_continuousMap`, `continuous_lintegral_boundedContinuousFunction`, `continuous_lintegral_continuousMap`, `continuous_map`, `continuous_mass`, `continuous_testAgainstNN_eval`, `ennreal_coeFn_eq_coeFn_toMeasure`, `ennreal_mass`, `eq_of_forall_apply_eq`, `eq_of_forall_toMeasure_apply_eq`, `eq_of_forall_toMeasure_apply_eq_iff`, `ext_of_forall_integral_eq`, `ext_of_forall_lintegral_eq`, `injective_toWeakDualBCNN`, `instContinuousAdd`, `instContinuousSMulNNReal`, `instR1Space`, `isEmbedding_toWeakDualBCNN`, `isFiniteMeasure`, `map_add`, `map_apply`, `map_apply'`, `map_apply_of_aemeasurable`, `map_smul`, `mass_comap_le`, `mass_map_le`, `mass_nonzero_iff`, `mass_zero_iff`, `measurableSet_isFiniteMeasure`, `measurable_fun_prod`, `measureReal_eq_coe_coeFn`, `mk_apply`, `mono_null`, `null_iff_toMeasure_null`, `pos_mono`, `restrict_apply`, `restrict_apply_measure`, `restrict_biUnion_finset`, `restrict_eq_zero_iff`, `restrict_mass`, `restrict_measure_eq`, `restrict_nonzero_iff`, `restrict_union`, `restrict_univ`, `smul_apply`, `smul_testAgainstNN_apply`, `t2Space`, `tendsto_iff_forall_integral_rclike_tendsto`, `tendsto_iff_forall_integral_tendsto`, `tendsto_iff_forall_lintegral_tendsto`, `tendsto_iff_forall_testAgainstNN_tendsto`, `tendsto_iff_forall_toWeakDualBCNN_tendsto`, `tendsto_iff_weakDual_tendsto`, `tendsto_lintegral_nn_of_le_const`, `tendsto_map_of_tendsto_of_continuous`, `tendsto_measure_iUnion_accumulate`, `tendsto_of_forall_integral_tendsto`, `tendsto_testAgainstNN_filter_of_le_const`, `tendsto_testAgainstNN_of_le_const`, `tendsto_zero_of_tendsto_zero_mass`, `tendsto_zero_testAgainstNN_of_tendsto_zero_mass`, `testAgainstNN_add`, `testAgainstNN_coe_eq`, `testAgainstNN_const`, `testAgainstNN_lipschitz`, `testAgainstNN_lipschitz_estimate`, `testAgainstNN_mono`, `testAgainstNN_one`, `testAgainstNN_smul`, `testAgainstNN_zero`, `toMeasureAddMonoidHom_apply`, `toMeasure_add`, `toMeasure_comap`, `toMeasure_injective`, `toMeasure_map`, `toMeasure_mk`, `toMeasure_smul`, `toMeasure_sum`, `toMeasure_zero`, `toWeakDualBCNN_apply`, `toWeakDualBCNN_continuous`, `val_eq_toMeasure`, `zero_mass`, `zero_testAgainstNN`, `zero_testAgainstNN_apply`, `continuousOn_comap_finiteMeasure`	103
Total	124

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mass` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `MeasureTheory.FiniteMeasure.instTopologicalSpace`	`NNReal` `MeasureTheory.FiniteMeasure.mass` `NNReal.instTopologicalSpace`	—	`comp` `Continuous.tendsto` `MeasureTheory.FiniteMeasure.continuous_mass`

MeasureTheory

Definitions

Name	Category	Theorems
`FiniteMeasure` 📖	CompOp	92 math math: `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure`, `isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le`, `FiniteMeasure.t2Space`, `isCompact_setOf_finiteMeasure_le_of_isCompact`, `FiniteMeasure.zero_testAgainstNN`, `FiniteMeasure.instR1Space`, `ProbabilityMeasure.range_toFiniteMeasure`, `FiniteMeasure.continuous_testAgainstNN_eval`, `FiniteMeasure.restrict_biUnion_finset`, `FiniteMeasure.injective_toWeakDualBCNN`, `FiniteMeasure.tendsto_iff_weakDual_tendsto`, `FiniteMeasure.tendsto_measure_iUnion_accumulate`, `FiniteMeasure.normalize_eq_of_nonzero`, `ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn`, `FiniteMeasure.tendsto_iff_forall_lintegral_tendsto`, `FiniteMeasure.self_eq_mass_smul_normalize`, `FiniteMeasure.self_eq_mass_mul_normalize`, `FiniteMeasure.pi_pi`, `FiniteMeasure.map_fst_prod`, `isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le`, `FiniteMeasure.tendsto_normalize_iff_tendsto`, `FiniteMeasure.tendsto_iff_forall_integral_tendsto`, `FiniteMeasure.coeFn_def`, `LevyProkhorov.edist_finiteMeasure_def`, `FiniteMeasure.zero_testAgainstNN_apply`, `FiniteMeasure.toMeasure_add`, `ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `FiniteMeasure.coeFn_zero`, `ProbabilityMeasure.toFiniteMeasure_apply`, `FiniteMeasure.continuous_iff_forall_continuous_lintegral`, `FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral`, `isCompact_setOf_finiteMeasure_eq_of_compactSpace`, `FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, `FiniteMeasure.apply_mono`, `FiniteMeasure.instContinuousSMulNNReal`, `isCompact_setOf_finiteMeasure_le_of_compactSpace`, `FiniteMeasure.restrict_eq_zero_iff`, `FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure`, `FiniteMeasure.toMeasure_injective`, `FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure`, `FiniteMeasure.tendsto_zero_of_tendsto_zero_mass`, `FiniteMeasure.prod_apply`, `FiniteMeasure.smul_testAgainstNN_apply`, `FiniteMeasure.coeFn_smul`, `FiniteMeasure.restrict_apply`, `FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero`, `FiniteMeasure.restrict_mass`, `FiniteMeasure.coeFn_add`, `FiniteMeasure.instContinuousAdd`, `FiniteMeasure.map_apply`, `FiniteMeasure.restrict_union`, `FiniteMeasure.smul_apply`, `FiniteMeasure.measureReal_eq_coe_coeFn`, `FiniteMeasure.mk_apply`, `FiniteMeasure.zero_mass`, `FiniteMeasure.continuous_map`, `FiniteMeasure.map_smul`, `FiniteMeasure.prod_apply_symm`, `FiniteMeasure.coeFn_mk`, `FiniteMeasure.continuous_lintegral_continuousMap`, `FiniteMeasure.prod_prod`, `FiniteMeasure.continuous_integral_boundedContinuousFunction`, `FiniteMeasure.apply_le_mass`, `FiniteMeasure.continuous_mass`, `FiniteMeasure.toWeakDualBCNN_continuous`, `FiniteMeasure.toMeasure_smul`, `ProbabilityMeasure.coeFn_toFiniteMeasure`, `FiniteMeasure.map_add`, `FiniteMeasure.isEmbedding_toWeakDualBCNN`, `ProbabilityMeasure.toFiniteMeasure_isEmbedding`, `ProbabilityMeasure.toFiniteMeasure_continuous`, `FiniteMeasure.mass_zero_iff`, `FiniteMeasure.continuous_iff_forall_continuousMap_continuous_integral`, `FiniteMeasure.tendsto_of_forall_integral_tendsto`, `FiniteMeasure.continuous_integral_continuousMap`, `FiniteMeasure.continuous_iff_forall_continuous_integral`, `FiniteMeasure.toMeasure_zero`, `FiniteMeasure.measurable_fun_prod`, `FiniteMeasure.map_snd_prod`, `FiniteMeasure.map_apply_of_aemeasurable`, `ProbabilityMeasure.toFiniteMeasure_apply_eq_apply`, `FiniteMeasure.toMeasure_sum`, `FiniteMeasure.zero_prod`, `FiniteMeasure.toMeasureAddMonoidHom_apply`, `FiniteMeasure.apply_union_le`, `FiniteMeasure.continuous_lintegral_boundedContinuousFunction`, `FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto`, `FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto`, `LevyProkhorov.dist_finiteMeasure_def`, `FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto`, `FiniteMeasure.prod_zero`, `FiniteMeasure.null_iff_toMeasure_null`

MeasureTheory.FiniteMeasure

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	3 math math: `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure`, `mass_comap_le`, `toMeasure_comap`
`instAdd` 📖	CompOp	5 math math: `toMeasure_add`, `coeFn_add`, `instContinuousAdd`, `restrict_union`, `map_add`
`instAddCommMonoid` 📖	CompOp	3 math math: `restrict_biUnion_finset`, `toMeasure_sum`, `toMeasureAddMonoidHom_apply`
`instCoe` 📖	CompOp	—
`instFunLike` 📖	CompOp	33 math math: `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure`, `isCompact_setOf_finiteMeasure_le_of_isCompact`, `tendsto_measure_iUnion_accumulate`, `normalize_eq_of_nonzero`, `MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn`, `self_eq_mass_mul_normalize`, `pi_pi`, `map_fst_prod`, `coeFn_def`, `coeFn_zero`, `MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply`, `apply_mono`, `restrict_eq_zero_iff`, `ennreal_coeFn_eq_coeFn_toMeasure`, `prod_apply`, `coeFn_smul`, `restrict_apply`, `restrict_mass`, `coeFn_add`, `map_apply`, `smul_apply`, `measureReal_eq_coe_coeFn`, `mk_apply`, `prod_apply_symm`, `coeFn_mk`, `prod_prod`, `apply_le_mass`, `MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure`, `map_snd_prod`, `map_apply_of_aemeasurable`, `MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply_eq_apply`, `apply_union_le`, `null_iff_toMeasure_null`
`instInhabited` 📖	CompOp	—
`instMeasurableSpace` 📖	CompOp	1 math math: `measurable_fun_prod`
`instModuleNNReal` 📖	CompOp	—
`instSMul` 📖	CompOp	10 math math: `self_eq_mass_smul_normalize`, `map_fst_prod`, `instContinuousSMulNNReal`, `smul_testAgainstNN_apply`, `coeFn_smul`, `normalize_eq_inv_mass_smul_of_nonzero`, `smul_apply`, `map_smul`, `toMeasure_smul`, `map_snd_prod`
`instTopologicalSpace` 📖	CompOp	37 math math: `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure`, `isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le`, `t2Space`, `isCompact_setOf_finiteMeasure_le_of_isCompact`, `instR1Space`, `continuous_testAgainstNN_eval`, `tendsto_iff_weakDual_tendsto`, `tendsto_iff_forall_lintegral_tendsto`, `isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le`, `tendsto_normalize_iff_tendsto`, `tendsto_iff_forall_integral_tendsto`, `MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `continuous_iff_forall_continuous_lintegral`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `isCompact_setOf_finiteMeasure_eq_of_compactSpace`, `tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, `instContinuousSMulNNReal`, `isCompact_setOf_finiteMeasure_le_of_compactSpace`, `Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure`, `tendsto_zero_of_tendsto_zero_mass`, `instContinuousAdd`, `continuous_map`, `continuous_lintegral_continuousMap`, `continuous_integral_boundedContinuousFunction`, `continuous_mass`, `toWeakDualBCNN_continuous`, `isEmbedding_toWeakDualBCNN`, `MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding`, `MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous`, `continuous_iff_forall_continuousMap_continuous_integral`, `tendsto_of_forall_integral_tendsto`, `continuous_integral_continuousMap`, `continuous_iff_forall_continuous_integral`, `continuous_lintegral_boundedContinuousFunction`, `tendsto_iff_forall_testAgainstNN_tendsto`, `tendsto_iff_forall_toWeakDualBCNN_tendsto`, `tendsto_iff_forall_integral_rclike_tendsto`
`instZero` 📖	CompOp	10 math math: `zero_testAgainstNN`, `zero_testAgainstNN_apply`, `coeFn_zero`, `restrict_eq_zero_iff`, `tendsto_zero_of_tendsto_zero_mass`, `zero_mass`, `mass_zero_iff`, `toMeasure_zero`, `zero_prod`, `prod_zero`
`map` 📖	CompOp	15 math math: `mass_map_le`, `prod_swap`, `map_fst_prod`, `Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure`, `map_apply`, `continuous_map`, `map_smul`, `map_apply'`, `map_add`, `toMeasure_map`, `pi_map_pi`, `map_snd_prod`, `map_apply_of_aemeasurable`, `map_prod_map`, `tendsto_map_of_tendsto_of_continuous`
`mapCLM` 📖	CompOp	—
`mapHom` 📖	CompOp	—
`mass` 📖	CompOp	30 math math: `mass_map_le`, `MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure`, `isCompact_setOf_finiteMeasure_mass_eq_compl_isCompact_le`, `Filter.Tendsto.mass`, `isCompact_setOf_finiteMeasure_le_of_isCompact`, `MeasureTheory.ProbabilityMeasure.range_toFiniteMeasure`, `testAgainstNN_eq_mass_mul`, `mass_prod`, `testAgainstNN_const`, `normalize_eq_of_nonzero`, `self_eq_mass_smul_normalize`, `self_eq_mass_mul_normalize`, `isCompact_setOf_finiteMeasure_mass_le_compl_isCompact_le`, `tendsto_normalize_iff_tendsto`, `isCompact_setOf_finiteMeasure_eq_of_compactSpace`, `isCompact_setOf_finiteMeasure_le_of_compactSpace`, `mass_comap_le`, `toMeasure_normalize_eq_of_nonzero`, `normalize_eq_inv_mass_smul_of_nonzero`, `restrict_mass`, `testAgainstNN_one`, `testAgainstNN_lipschitz`, `zero_mass`, `normalize_testAgainstNN`, `apply_le_mass`, `continuous_mass`, `mass_zero_iff`, `ennreal_mass`, `testAgainstNN_lipschitz_estimate`, `mass_pi`
`restrict` 📖	CompOp	8 math math: `restrict_apply_measure`, `restrict_biUnion_finset`, `restrict_univ`, `restrict_eq_zero_iff`, `restrict_apply`, `restrict_mass`, `restrict_measure_eq`, `restrict_union`
`testAgainstNN` 📖	CompOp	25 math math: `zero_testAgainstNN`, `tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, `continuous_testAgainstNN_eval`, `testAgainstNN_eq_mass_mul`, `testAgainstNN_const`, `testAgainstNN_coe_eq`, `zero_testAgainstNN_apply`, `testAgainstNN_add`, `tendsto_zero_testAgainstNN_of_tendsto_zero_mass`, `testAgainstNN_mono`, `testAgainstNN_zero`, `smul_testAgainstNN_apply`, `tendsto_testAgainstNN_filter_of_le_const`, `MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN`, `testAgainstNN_one`, `tendsto_testAgainstNN_of_le_const`, `testAgainstNN_lipschitz`, `tendsto_normalize_testAgainstNN_of_tendsto`, `normalize_testAgainstNN`, `MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz`, `MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval`, `testAgainstNN_smul`, `testAgainstNN_lipschitz_estimate`, `coe_toWeakDualBCNN`, `tendsto_iff_forall_testAgainstNN_tendsto`
`toMeasure` 📖	CompOp	44 math math: `MeasureTheory.ProbabilityMeasure.toMeasure_comp_toFiniteMeasure_eq_toMeasure`, `toWeakDualBCNN_apply`, `restrict_apply_measure`, `tendsto_iff_forall_lintegral_tendsto`, `eq_of_forall_toMeasure_apply_eq_iff`, `testAgainstNN_coe_eq`, `tendsto_iff_forall_integral_tendsto`, `coeFn_def`, `MeasureTheory.LevyProkhorov.edist_finiteMeasure_def`, `toMeasure_mk`, `toMeasure_add`, `continuous_iff_forall_continuous_lintegral`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `limsup_measure_closed_le_of_tendsto`, `average_eq_integral_normalize`, `ennreal_coeFn_eq_coeFn_toMeasure`, `toMeasure_injective`, `tendsto_lintegral_nn_of_le_const`, `val_eq_toMeasure`, `prod_apply`, `toMeasure_normalize_eq_of_nonzero`, `restrict_measure_eq`, `measureReal_eq_coe_coeFn`, `prod_apply_symm`, `continuous_lintegral_continuousMap`, `continuous_integral_boundedContinuousFunction`, `toMeasure_smul`, `toMeasure_map`, `ennreal_mass`, `continuous_iff_forall_continuousMap_continuous_integral`, `continuous_integral_continuousMap`, `toMeasure_pi`, `toMeasure_comap`, `continuous_iff_forall_continuous_integral`, `toMeasure_zero`, `measurable_fun_prod`, `isFiniteMeasure`, `toMeasure_sum`, `toMeasureAddMonoidHom_apply`, `continuous_lintegral_boundedContinuousFunction`, `MeasureTheory.LevyProkhorov.dist_finiteMeasure_def`, `tendsto_iff_forall_integral_rclike_tendsto`, `toMeasure_prod`, `null_iff_toMeasure_null`
`toMeasureAddMonoidHom` 📖	CompOp	1 math math: `toMeasureAddMonoidHom_apply`
`toWeakDualBCNN` 📖	CompOp	7 math math: `toWeakDualBCNN_apply`, `injective_toWeakDualBCNN`, `tendsto_iff_weakDual_tendsto`, `toWeakDualBCNN_continuous`, `isEmbedding_toWeakDualBCNN`, `coe_toWeakDualBCNN`, `tendsto_iff_forall_toWeakDualBCNN_tendsto`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_iUnion_le` 📖	mathematical	`Summable` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instTopologicalSpace` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `instFunLike` `SummationFilter.unconditional`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.iUnion` `tsum`	—	`ennreal_coeFn_eq_coeFn_toMeasure` `ENNReal.coe_tsum` `MeasureTheory.measure_iUnion_le` `MeasureTheory.Measure.instOuterMeasureClass` `instCountableNat`
`apply_le_mass` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `instFunLike` `mass`	—	`apply_mono` `Set.subset_univ`
`apply_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `instFunLike`	—	`ENNReal.toNNReal_mono` `MeasureTheory.measure_ne_top` `isFiniteMeasure` `MeasureTheory.OuterMeasure.mono`
`apply_union_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `instFunLike` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`MeasureTheory.measure_union_le` `MeasureTheory.Measure.instOuterMeasureClass` `LE.le.trans_eq` `ENNReal.toNNReal_mono` `ENNReal.Finiteness.add_ne_top` `MeasureTheory.measure_ne_top` `isFiniteMeasure` `ENNReal.toNNReal_add` `coeFn_def`
`coeFn_add` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `instAdd` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`ennreal_coeFn_eq_coeFn_toMeasure`
`coeFn_def` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `ENNReal.toNNReal` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	—
`coeFn_mk` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `MeasureTheory.IsFiniteMeasure` `ENNReal.toNNReal` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—
`coeFn_smul` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `instSMul` `Function.hasSMul`	—	`ennreal_coeFn_eq_coeFn_toMeasure` `ENNReal.coe_smul`
`coeFn_zero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `instZero` `Pi.instZero` `instZeroNNReal`	—	—
`coe_toWeakDualBCNN` 📖	mathematical	—	`DFunLike.coe` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instFunLikeWeakDual` `toWeakDualBCNN` `testAgainstNN`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`continuous_iff_forall_continuousMap_continuous_integral` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	`continuous_iff_forall_continuous_integral` `Equiv.forall_congr_left`
`continuous_iff_forall_continuousMap_continuous_lintegral` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `ENNReal` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `ContinuousMap` `NNReal` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike`	—	`continuous_iff_forall_continuous_lintegral` `Equiv.forall_congr_left`
`continuous_iff_forall_continuous_integral` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike`	—	`forall_swap`
`continuous_iff_forall_continuous_lintegral` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `ENNReal` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	`forall_swap`
`continuous_integral_boundedContinuousFunction` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike`	—	`continuous_iff_forall_continuous_integral` `continuous_id`
`continuous_integral_continuousMap` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe`	—	`continuous_iff_forall_continuousMap_continuous_integral` `continuous_id` `ContinuousMapClass.map_continuous`
`continuous_lintegral_boundedContinuousFunction` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	`continuous_iff_forall_continuous_lintegral` `continuous_id`
`continuous_lintegral_continuousMap` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `NNReal`	—	`continuous_iff_forall_continuousMap_continuous_lintegral` `continuous_id` `ContinuousMapClass.map_continuous`
`continuous_map` 📖	mathematical	`Continuous`	`MeasureTheory.FiniteMeasure` `instTopologicalSpace` `BorelSpace.opensMeasurable` `map`	—	`BorelSpace.opensMeasurable` `continuous_iff_continuousAt` `tendsto_map_of_tendsto_of_continuous` `Continuous.continuousAt` `continuous_id`
`continuous_mass` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `NNReal` `instTopologicalSpace` `NNReal.instTopologicalSpace` `mass`	—	`continuous_testAgainstNN_eval`
`continuous_testAgainstNN_eval` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `NNReal` `instTopologicalSpace` `NNReal.instTopologicalSpace` `testAgainstNN`	—	`Continuous.comp` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `WeakBilin.eval_continuous` `toWeakDualBCNN_continuous`
`ennreal_coeFn_eq_coeFn_toMeasure` 📖	mathematical	—	`ENNReal.ofNNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`ENNReal.coe_toNNReal` `LT.lt.ne` `MeasureTheory.measure_lt_top` `isFiniteMeasure`
`ennreal_mass` 📖	mathematical	—	`ENNReal.ofNNReal` `mass` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `Set.univ`	—	`ennreal_coeFn_eq_coeFn_toMeasure`
`eq_of_forall_apply_eq` 📖	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike`	—	—	`eq_of_forall_toMeasure_apply_eq` `ennreal_coeFn_eq_coeFn_toMeasure`
`eq_of_forall_toMeasure_apply_eq` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	—	`MeasureTheory.Measure.ext`
`eq_of_forall_toMeasure_apply_eq_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`eq_of_forall_toMeasure_apply_eq`
`ext_of_forall_integral_eq` 📖	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike`	—	—	`ext_of_forall_lintegral_eq` `ENNReal.toReal_eq_toReal_iff'` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `isFiniteMeasure` `BoundedContinuousFunction.toReal_lintegral_coe_eq_integral` `BorelSpace.opensMeasurable` `Continuous.comp'` `NNReal.continuous_coe` `BoundedContinuousFunction.continuous` `BoundedContinuousFunction.map_bounded'`
`ext_of_forall_lintegral_eq` 📖	—	`MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	—	`MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure` `isFiniteMeasure`
`injective_toWeakDualBCNN` 📖	mathematical	—	`MeasureTheory.FiniteMeasure` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `toWeakDualBCNN` `BorelSpace.opensMeasurable`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `BorelSpace.opensMeasurable` `ext_of_forall_lintegral_eq` `ENNReal.toNNReal_eq_toNNReal_iff'` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `isFiniteMeasure`
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `instAdd`	—	`continuous_iff_continuousAt` `tendsto_iff_forall_lintegral_tendsto` `nhds_prod_eq` `Filter.Tendsto.comp` `Filter.tendsto_id` `Filter.tendsto_fst` `Filter.tendsto_snd` `MeasureTheory.lintegral_add_measure` `Filter.Tendsto.add` `ENNReal.instContinuousAdd`
`instContinuousSMulNNReal` 📖	mathematical	—	`ContinuousSMul` `NNReal` `MeasureTheory.FiniteMeasure` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `ENNReal` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `ENNReal.instMulActionNNReal` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `ENNReal.instAddCommMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.right` `NNReal.instTopologicalSpace` `instTopologicalSpace`	—	`IsScalarTower.left` `IsScalarTower.right` `continuous_iff_continuousAt` `tendsto_iff_forall_integral_tendsto` `nhds_prod_eq` `Filter.tendsto_fst` `Filter.Tendsto.comp` `Filter.tendsto_id` `Filter.tendsto_snd` `MeasureTheory.integral_smul_nnreal_measure` `Filter.Tendsto.smul` `NNReal.instContinuousSMulOfReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`instR1Space` 📖	mathematical	—	`R1Space` `MeasureTheory.FiniteMeasure` `instTopologicalSpace`	—	`Topology.IsInducing.r1Space` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `T2Space.r1Space` `WeakDual.instT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`isEmbedding_toWeakDualBCNN` 📖	mathematical	—	`Topology.IsEmbedding` `MeasureTheory.FiniteMeasure` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instTopologicalSpace` `BorelSpace.opensMeasurable` `instTopologicalSpaceWeakDual` `toWeakDualBCNN`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `BorelSpace.opensMeasurable` `injective_toWeakDualBCNN`
`isFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `toMeasure`	—	`Subtype.prop`
`map_add` 📖	mathematical	`Measurable`	`map` `MeasureTheory.FiniteMeasure` `instAdd`	—	`eq_of_forall_toMeasure_apply_eq` `MeasureTheory.Measure.map_add` `MeasureTheory.Measure.map_apply`
`map_apply` 📖	mathematical	`Measurable` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `map` `Set.preimage`	—	`map_apply_of_aemeasurable` `Measurable.aemeasurable`
`map_apply'` 📖	mathematical	`AEMeasurable` `toMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `map` `Set.preimage`	—	`MeasureTheory.Measure.map_apply_of_aemeasurable`
`map_apply_of_aemeasurable` 📖	mathematical	`AEMeasurable` `toMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `map` `Set.preimage`	—	`map_apply'` `ENNReal.toNNReal_eq_toNNReal_iff'` `MeasureTheory.measure_ne_top` `isFiniteMeasure`
`map_smul` 📖	mathematical	—	`map` `NNReal` `MeasureTheory.FiniteMeasure` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `ENNReal` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `ENNReal.instMulActionNNReal` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `ENNReal.instAddCommMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.right`	—	`eq_of_forall_toMeasure_apply_eq` `IsScalarTower.left` `IsScalarTower.right` `MeasureTheory.Measure.map_smul`
`mass_comap_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `mass` `comap`	—	`MeasureTheory.IsFiniteMeasure_comap` `isFiniteMeasure` `LE.le.trans` `MeasureTheory.Measure.comap_apply_le` `MeasureTheory.nullMeasurableSet_univ` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_univ`
`mass_map_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `mass` `map`	—	`MeasureTheory.Measure.isFiniteMeasure_map` `isFiniteMeasure` `MeasureTheory.Measure.map_apply_of_aemeasurable` `MeasurableSet.univ` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_univ` `MeasureTheory.Measure.map_of_not_aemeasurable` `ENNReal.instCanonicallyOrderedAdd`
`mass_nonzero_iff` 📖	—	—	—	—	`not_iff_not` `mass_zero_iff`
`mass_zero_iff` 📖	mathematical	—	`mass` `NNReal` `instZeroNNReal` `MeasureTheory.FiniteMeasure` `instZero`	—	`toMeasure_injective` `MeasureTheory.Measure.measure_univ_eq_zero` `ennreal_mass` `ENNReal.coe_eq_zero`
`measurableSet_isFiniteMeasure` 📖	mathematical	—	`MeasurableSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instMeasurableSpace` `setOf` `MeasureTheory.IsFiniteMeasure`	—	`Set.ext` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.isFiniteMeasure_iff` `MeasureTheory.Measure.measurable_coe` `MeasurableSet.univ` `measurableSet_Ico` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology`
`measurable_fun_prod` 📖	mathematical	—	`Measurable` `MeasureTheory.FiniteMeasure` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instMeasurableSpace` `MeasureTheory.Measure.instMeasurableSpace` `MeasureTheory.Measure.prod` `toMeasure`	—	`Measurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.comp` `MeasureTheory.Measure.measurable_coe` `measurable_subtype_coe` `measurable_fst` `measurable_snd` `Measurable.measure_of_isPiSystem` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `isFiniteMeasure` `generateFrom_prod` `isPiSystem_prod` `MeasureTheory.Measure.prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasurableSet.univ`
`measureReal_eq_coe_coeFn` 📖	mathematical	—	`MeasureTheory.Measure.real` `toMeasure` `NNReal.toReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike`	—	—
`mk_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `MeasureTheory.IsFiniteMeasure` `ENNReal.toNNReal` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—
`mono_null` 📖	—	`Set` `Set.instHasSubset` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `NNReal` `instFunLike` `instZeroNNReal`	—	—	`eq_bot_mono` `apply_mono`
`null_iff_toMeasure_null` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `instZeroNNReal` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `instZeroENNReal`	—	`ennreal_coeFn_eq_coeFn_toMeasure` `ENNReal.coe_zero`
`pos_mono` 📖	—	`Set` `Set.instHasSubset` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `instFunLike`	—	—	`LT.lt.trans_le` `apply_mono`
`restrict_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `restrict` `Set.instInter`	—	`MeasureTheory.Measure.restrict_apply`
`restrict_apply_measure` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `restrict` `Set.instInter`	—	`MeasureTheory.Measure.restrict_apply`
`restrict_biUnion_finset` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet`	`restrict` `Set.iUnion` `Finset.instMembership` `Finset.sum` `MeasureTheory.FiniteMeasure` `instAddCommMonoid`	—	`eq_of_forall_toMeasure_apply_eq` `toMeasure_sum` `Finset.sum_congr` `MeasureTheory.Measure.coe_finset_sum` `Finset.sum_apply` `MeasureTheory.Measure.restrict_biUnion_finset` `MeasureTheory.Measure.sum_fintype` `Finset.sum_attach`
`restrict_eq_zero_iff` 📖	mathematical	—	`restrict` `MeasureTheory.FiniteMeasure` `instZero` `DFunLike.coe` `Set` `NNReal` `instFunLike` `instZeroNNReal`	—	`mass_zero_iff` `restrict_mass`
`restrict_mass` 📖	mathematical	—	`mass` `restrict` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike`	—	`restrict_apply` `MeasurableSet.univ` `Set.univ_inter`
`restrict_measure_eq` 📖	mathematical	—	`toMeasure` `restrict` `MeasureTheory.Measure.restrict`	—	—
`restrict_nonzero_iff` 📖	—	—	—	—	—
`restrict_union` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet`	`restrict` `Set.instUnion` `MeasureTheory.FiniteMeasure` `instAdd`	—	`eq_of_forall_toMeasure_apply_eq` `MeasureTheory.Measure.restrict_union`
`restrict_univ` 📖	mathematical	—	`restrict` `Set.univ`	—	`eq_of_forall_toMeasure_apply_eq` `MeasureTheory.Measure.restrict_univ`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `instSMul`	—	`coeFn_smul` `Pi.smul_apply`
`smul_testAgainstNN_apply` 📖	mathematical	—	`testAgainstNN` `NNReal` `MeasureTheory.FiniteMeasure` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `ENNReal` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `ENNReal.instMulActionNNReal` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `ENNReal.instAddCommMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.right`	—	`IsScalarTower.left` `IsScalarTower.right` `MeasureTheory.lintegral_smul_measure`
`t2Space` 📖	mathematical	—	`T2Space` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `BorelSpace.opensMeasurable`	—	`Topology.IsEmbedding.t2Space` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `BorelSpace.opensMeasurable` `WeakDual.instT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `isEmbedding_toWeakDualBCNN`
`tendsto_iff_forall_integral_rclike_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAlgebra.toNormedSpace` `Real` `Real.normedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `RCLike.toNormedAlgebra` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`tendsto_iff_forall_integral_tendsto` `integral_re_add_im` `BoundedContinuousFunction.integrable` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `RCLike.borelSpace` `isFiniteMeasure` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Filter.Tendsto.comp` `Continuous.tendsto` `RCLike.continuous_ofReal` `RCLike.lipschitzWith_re` `Filter.Tendsto.mul_const` `IsTopologicalSemiring.toContinuousMul` `RCLike.lipschitzWith_im` `Filter.tendsto_ofReal_iff'` `instBoundedMul` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `RCLike.lipschitzWith_ofReal` `integral_ofReal`
`tendsto_iff_forall_integral_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `Real` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`tendsto_iff_forall_lintegral_tendsto` `BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub` `isFiniteMeasure` `Filter.Tendsto.comp` `ENNReal.tendsto_toReal` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `BoundedContinuousFunction.toReal_lintegral_coe_eq_integral` `tendsto_of_forall_integral_tendsto`
`tendsto_iff_forall_lintegral_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `ENNReal` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `ENNReal.instTopologicalSpace`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `tendsto_iff_forall_toWeakDualBCNN_tendsto` `toWeakDualBCNN_apply`
`tendsto_iff_forall_testAgainstNN_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `NNReal` `testAgainstNN` `NNReal.instTopologicalSpace`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `tendsto_iff_forall_toWeakDualBCNN_tendsto`
`tendsto_iff_forall_toWeakDualBCNN_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `NNReal` `DFunLike.coe` `WeakDual` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instFunLikeWeakDual` `toWeakDualBCNN`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `tendsto_iff_weakDual_tendsto` `Algebra.to_smulCommClass` `tendsto_iff_forall_eval_tendsto_topDualPairing`
`tendsto_iff_weakDual_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `toWeakDualBCNN` `instTopologicalSpaceWeakDual`	—	`Topology.IsInducing.tendsto_nhds_iff` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`tendsto_lintegral_nn_of_le_const` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `NNReal.instTopologicalSpace`	`ENNReal` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `ENNReal.instTopologicalSpace`	—	`MeasureTheory.tendsto_lintegral_nn_filter_of_le_const` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `isFiniteMeasure` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass`
`tendsto_map_of_tendsto_of_continuous` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace` `Continuous`	`map` `BorelSpace.opensMeasurable`	—	`BorelSpace.opensMeasurable` `tendsto_iff_forall_lintegral_tendsto` `MeasureTheory.lintegral_map` `Continuous.measurable` `ENNReal.borelSpace` `Continuous.comp` `ENNReal.continuous_coe` `BoundedContinuousFunction.continuous`
`tendsto_measure_iUnion_accumulate` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `instFunLike` `Set.accumulate` `Preorder.toLE` `Filter.atTop` `nhds` `NNReal.instTopologicalSpace` `Set.iUnion`	—	`MeasureTheory.tendsto_measure_iUnion_accumulate`
`tendsto_of_forall_integral_tendsto` 📖	mathematical	`Filter.Tendsto` `Real` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`MeasureTheory.FiniteMeasure` `instTopologicalSpace`	—	`tendsto_iff_forall_lintegral_tendsto` `ENNReal.tendsto_toReal_iff` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `isFiniteMeasure` `Isometry.lipschitz` `isometry_subtype_coe` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.Eventually.of_forall` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Continuous.measurable` `BoundedContinuousFunction.continuous` `ENNReal.ofReal_coe_nnreal`
`tendsto_testAgainstNN_filter_of_le_const` 📖	mathematical	`Filter.Eventually` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `toMeasure` `Filter.Tendsto` `nhds` `NNReal.instTopologicalSpace`	`testAgainstNN`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.Tendsto.comp` `ENNReal.tendsto_toNNReal` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `isFiniteMeasure` `MeasureTheory.tendsto_lintegral_nn_filter_of_le_const`
`tendsto_testAgainstNN_of_le_const` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `NNReal.instTopologicalSpace`	`testAgainstNN`	—	`tendsto_testAgainstNN_filter_of_le_const` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass`
`tendsto_zero_of_tendsto_zero_mass` 📖	mathematical	`Filter.Tendsto` `NNReal` `mass` `nhds` `NNReal.instTopologicalSpace` `instZeroNNReal`	`MeasureTheory.FiniteMeasure` `instTopologicalSpace` `instZero`	—	`tendsto_iff_forall_testAgainstNN_tendsto` `zero_testAgainstNN_apply` `tendsto_zero_testAgainstNN_of_tendsto_zero_mass`
`tendsto_zero_testAgainstNN_of_tendsto_zero_mass` 📖	mathematical	`Filter.Tendsto` `NNReal` `mass` `nhds` `NNReal.instTopologicalSpace` `instZeroNNReal`	`testAgainstNN`	—	`tendsto_iff_dist_tendsto_zero` `testAgainstNN_lipschitz_estimate` `NNReal.nndist_zero_eq_val'` `squeeze_zero` `NNReal.coe_nonneg` `zero_add` `testAgainstNN_zero` `Prod.tendsto_iff` `tendsto_const_nhds` `Filter.Tendsto.comp` `Continuous.tendsto` `NNReal.continuous_coe` `MulZeroClass.mul_zero` `tendsto_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`testAgainstNN_add` 📖	mathematical	—	`testAgainstNN` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NNReal.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NNReal.instIsTopologicalSemiring`	—	`instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `testAgainstNN_coe_eq` `MeasureTheory.lintegral_add_left` `BoundedContinuousFunction.measurable_coe_ennreal_comp`
`testAgainstNN_coe_eq` 📖	mathematical	—	`ENNReal.ofNNReal` `testAgainstNN` `MeasureTheory.lintegral` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	`ENNReal.coe_toNNReal` `LT.lt.ne` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `isFiniteMeasure`
`testAgainstNN_const` 📖	mathematical	—	`testAgainstNN` `BoundedContinuousFunction.const` `NNReal` `instPseudoMetricSpaceNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `mass`	—	`testAgainstNN_coe_eq` `MeasureTheory.lintegral_const` `ennreal_mass`
`testAgainstNN_lipschitz` 📖	mathematical	—	`LipschitzWith` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `BoundedContinuousFunction.instMetricSpace` `instMetricSpaceNNReal` `mass` `testAgainstNN`	—	`lipschitzWith_iff_dist_le_mul` `abs_le` `Real.instIsOrderedAddMonoid` `testAgainstNN_lipschitz_estimate` `nndist_comm` `NNReal.coe_mono` `mul_comm` `le_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.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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_add_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `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` `NNReal.dist_eq`
`testAgainstNN_lipschitz_estimate` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `testAgainstNN` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Distrib.toMul` `NNDist.nndist` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `PseudoMetricSpace.toNNDist` `BoundedContinuousFunction.instPseudoMetricSpace` `mass`	—	`instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `testAgainstNN_const` `testAgainstNN_coe_eq` `coe_nnreal_ennreal_nndist` `MeasureTheory.lintegral_mono` `BoundedContinuousFunction.dist_coe_le_dist` `NNReal.le_add_nndist` `add_le_add_iff_left` `NNReal.addLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT`
`testAgainstNN_mono` 📖	mathematical	`Pi.hasLe` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	`testAgainstNN`	—	`testAgainstNN_coe_eq` `MeasureTheory.lintegral_mono_fn'` `le_refl` `ENNReal.coe_le_coe_of_le`
`testAgainstNN_one` 📖	mathematical	—	`testAgainstNN` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instOne` `instOneNNReal` `mass`	—	`MeasureTheory.lintegral_one`
`testAgainstNN_smul` 📖	mathematical	—	`testAgainstNN` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instSMul` `instZeroNNReal`	—	`testAgainstNN_coe_eq` `ENNReal.coe_smul` `smul_one_smul` `MeasureTheory.lintegral_const_mul` `BoundedContinuousFunction.measurable_coe_ennreal_comp`
`testAgainstNN_zero` 📖	mathematical	—	`testAgainstNN` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instZero` `instZeroNNReal`	—	`MulZeroClass.zero_mul` `testAgainstNN_const`
`toMeasureAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `MeasureTheory.FiniteMeasure` `MeasureTheory.Measure` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `MeasureTheory.Measure.instAddCommMonoid` `AddMonoidHom.instFunLike` `toMeasureAddMonoidHom` `toMeasure`	—	—
`toMeasure_add` 📖	mathematical	—	`toMeasure` `MeasureTheory.FiniteMeasure` `instAdd` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	—
`toMeasure_comap` 📖	mathematical	—	`toMeasure` `comap` `MeasureTheory.Measure.comap`	—	—
`toMeasure_injective` 📖	mathematical	—	`MeasureTheory.FiniteMeasure` `MeasureTheory.Measure` `toMeasure`	—	`Subtype.coe_injective`
`toMeasure_map` 📖	mathematical	—	`toMeasure` `map` `MeasureTheory.Measure.map`	—	—
`toMeasure_mk` 📖	mathematical	—	`toMeasure` `MeasureTheory.Measure` `MeasureTheory.IsFiniteMeasure`	—	—
`toMeasure_smul` 📖	mathematical	—	`toMeasure` `MeasureTheory.FiniteMeasure` `instSMul` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul`	—	—
`toMeasure_sum` 📖	mathematical	—	`toMeasure` `Finset.sum` `MeasureTheory.FiniteMeasure` `instAddCommMonoid` `MeasureTheory.Measure` `MeasureTheory.Measure.instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`toMeasure_zero` 📖	mathematical	—	`toMeasure` `MeasureTheory.FiniteMeasure` `instZero` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	—
`toWeakDualBCNN_apply` 📖	mathematical	—	`DFunLike.coe` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instFunLikeWeakDual` `toWeakDualBCNN` `ENNReal.toNNReal` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `BoundedContinuousFunction.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`toWeakDualBCNN_continuous` 📖	mathematical	—	`Continuous` `MeasureTheory.FiniteMeasure` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instTopologicalSpace` `instTopologicalSpaceWeakDual` `toWeakDualBCNN`	—	`continuous_induced_dom` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`val_eq_toMeasure` 📖	mathematical	—	`MeasureTheory.Measure` `MeasureTheory.IsFiniteMeasure` `toMeasure`	—	—
`zero_mass` 📖	mathematical	—	`mass` `MeasureTheory.FiniteMeasure` `instZero` `NNReal` `instZeroNNReal`	—	—
`zero_testAgainstNN` 📖	mathematical	—	`testAgainstNN` `MeasureTheory.FiniteMeasure` `instZero` `Pi.instZero` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `instZeroNNReal`	—	`zero_testAgainstNN_apply`
`zero_testAgainstNN_apply` 📖	mathematical	—	`testAgainstNN` `MeasureTheory.FiniteMeasure` `instZero` `NNReal` `instZeroNNReal`	—	`MeasureTheory.lintegral_zero_measure`

MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmbedding_map_finiteMeasure` 📖	mathematical	`Topology.IsClosedEmbedding`	`Topology.IsEmbedding` `MeasureTheory.FiniteMeasure` `MeasureTheory.FiniteMeasure.instTopologicalSpace` `BorelSpace.opensMeasurable` `MeasureTheory.FiniteMeasure.map`	—	`BorelSpace.opensMeasurable` `Topology.IsEmbedding.subtypeVal` `MeasureTheory.Measure.map_apply` `Continuous.measurable` `Topology.IsClosedEmbedding.continuous` `IsOpen.measurableSet` `IsClosed.isOpen_compl` `Topology.IsClosedEmbedding.isClosed_range` `Set.preimage_range` `Set.compl_univ` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq` `MeasureTheory.Measure.comap_apply` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `MeasurableEmbedding.measurableSet_image'` `Topology.IsClosedEmbedding.measurableEmbedding` `Set.preimage_image_eq` `Set.image_preimage_eq_inter_range` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.Measure.restrict_eq_self_of_ae_mem` `MeasureTheory.FiniteMeasure.null_iff_toMeasure_null` `MeasureTheory.FiniteMeasure.continuous_map` `continuousOn_iff_continuous_restrict` `Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure` `Topology.IsEmbedding.comp` `Homeomorph.isEmbedding`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_comap_finiteMeasure` 📖	mathematical	`Topology.IsClosedEmbedding`	`ContinuousOn` `MeasureTheory.FiniteMeasure` `MeasureTheory.FiniteMeasure.instTopologicalSpace` `BorelSpace.opensMeasurable` `MeasureTheory.FiniteMeasure.comap` `setOf` `NNReal` `DFunLike.coe` `Set` `MeasureTheory.FiniteMeasure.instFunLike` `Compl.compl` `Set.instCompl` `Set.range` `instZeroNNReal`	—	`BorelSpace.opensMeasurable` `MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto` `BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding` `MeasurableEmbedding.integral_map` `measurableEmbedding` `MeasurableEmbedding.map_comap` `MeasureTheory.Measure.restrict_eq_self_of_ae_mem` `nhdsWithin.eq_1` `Filter.tendsto_id` `Filter.Tendsto.mono_left` `inf_le_left` `Filter.Tendsto.congr'` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'`

---

← Back to Index